1  /-
  2  Copyright (c) 2018 Chris Hughes. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Chris Hughes
  5  -/
  6  import data.fintype
src         └──────────┘
  7  
  8  universes u v
  9  open equiv function fintype finset
 10  variables {α : Type u} {β : Type v}
 11  
 12  namespace equiv.perm
 13  
 14  def subtype_perm (f : perm α) {p : α → Prop} (h : ∀ x, p x ↔ p (f x)) : perm {x // p x} :=
 15  ⟨λ x, ⟨f x, (h _).1 x.2⟩, λ x, ⟨f⁻¹ x, (h (f⁻¹ x)).2 $ by simpa using x.2⟩,
src                                                            └──────────┘ └┘
typ                                                            └──────────┘ └┘
doc                                                            └──────────┘ └┘
txt                                                            └──────────┘ └┘
par                                                            └──────────┘ └┘
pid                                                                 └────┘ └┘
 16    λ _, by simp, λ _, by simp⟩
id                     
src            └──┘          └──┘
typ            └──┘         └──┘
doc            └──┘          └──┘
txt            └──┘          └──┘
par            └──┘          └──┘
st                         └───┘
 17  
 18  @[simp] lemma subtype_perm_one (p : α → Prop) (h : ∀ x, p x ↔ p ((1 : perm α) x)) : @subtype_perm α 1 p h = 1 :=
id                                                                   └──┘         └──────────┘      
src                                                                       └──┘           └──────────┘         
typ                                                                  └──┘         └──────────┘      
doc    └──┘                                                                └──┘
 19  equiv.ext _ _ $ λ ⟨_, _⟩, rfl
id   └───────┘                └─┘
src  └───────┘                 └─┘
typ  └───────┘                └─┘
 20  
 21  def of_subtype {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) : perm α :=
 22  ⟨λ x, if h : p x then f ⟨x, h⟩ else x, λ x, if h : p x then f⁻¹ ⟨x, h⟩ else x,
 23    λ x, have h : ∀ h : p x, p (f ⟨x, h⟩), from λ h, (f ⟨x, h⟩).2,
 24      by simp; split_ifs at *; simp * at *,
src         └──┘  └────────────┘  └─────────┘
typ         └──┘  └────────────┘  └─────────┘
doc         └──┘  └────────────┘  └─────────┘
txt         └──┘  └────────────┘  └─────────┘
par         └──┘  └────────────┘  └─────────┘
pid                        └───┘      └──┘
 25    λ x, have h : ∀ h : p x, p (f⁻¹ ⟨x, h⟩), from λ h, (f⁻¹ ⟨x, h⟩).2,
 26      by simp; split_ifs at *; simp * at *⟩
src         └──┘  └────────────┘  └─────────┘
typ         └──┘  └────────────┘  └─────────┘
doc         └──┘  └────────────┘  └─────────┘
txt         └──┘  └────────────┘  └─────────┘
par         └──┘  └────────────┘  └─────────┘
pid                        └───┘      └──┘
st                           └──────────────┘
 27  
 28  instance of_subtype.is_group_hom {p : α → Prop} [decidable_pred p] : is_group_hom (@of_subtype α p _) :=
 29  { map_mul := λ f g, equiv.ext _ _ $ λ x, begin
 30    rw [of_subtype, of_subtype, of_subtype],
src    └──┘          └┘          └┘          
typ    └──┘          └┘          └┘          
doc    └──┘          └┘          └┘          
txt    └──┘          └┘          └┘          
par    └──┘          └┘          └┘          
pid      └┘          └┘          └┘          
 31    by_cases h : p x,
src    └───────┘ └─┘ 
typ    └───────┘ └─┘ 
doc    └───────┘ └─┘ 
txt    └───────┘ └─┘ 
par    └───────┘ └─┘ 
pid             └─┘ 
 32    { have h₁ : p (f (g ⟨x, h⟩)), from (f (g ⟨x, h⟩)).2,
id                                          
src      └────────┘       └┘ └─┘  └───┘      └┘ └───┘
typ      └────────┘   └┘└─┘  └───┘   └┘└───┘
doc      └────────┘       └┘ └─┘  └───┘      └┘ └───┘
txt      └────────┘       └┘ └─┘  └───┘      └┘ └───┘
par      └────────┘       └┘ └─┘  └───┘      └┘ └───┘
pid      └─────┘└─┘       └┘ └─┘  └───┘      └┘ └─┘└┘
st        └───────────────────────┘└─────────────────────┘└─
 33      have h₂ : p (g ⟨x, h⟩), from (g ⟨x, h⟩).2,
id                                     
src      └────────┘     └┘ └┘  └───┘    └┘ └──┘
typ      └────────┘  └┘└┘  └───┘  └┘└──┘
doc      └────────┘     └┘ └┘  └───┘    └┘ └──┘
txt      └────────┘     └┘ └┘  └───┘    └┘ └──┘
par      └────────┘     └┘ └┘  └───┘    └┘ └──┘
pid      └─────┘└─┘     └┘ └┘  └───┘    └┘ └┘└┘
st   ─────────────────────────┘└─────────────────┘└─
 34      simp [h, h₁, h₂] },
id               └┘  └┘
src      └────┘ └┘  └┘  └┘
typ      └────┘└┘└┘└┘└┘└┘
doc      └────┘ └┘  └┘  └┘
txt      └────┘ └┘  └┘  └┘
par      └────┘ └┘  └┘  └┘
pid           └┘  └┘  
st   ────────────────────┘└┘
 35    { simp [h] }
id             
src      └────┘ └┘
typ      └────┘└┘
doc      └────┘ └┘
txt      └────┘ └┘
par      └────┘ └┘
pid           
st   ────────────┘└─
 36  end }
st   ──┘
 37  
 38  @[simp] lemma of_subtype_one (p : α → Prop) [decidable_pred p] : @of_subtype α p _ 1 = 1 :=
id                                               └────────────┘      └────────┘       
src                                               └────────────┘       └────────┘         
typ                                              └────────────┘      └────────┘       
doc    └──┘
 39  is_group_hom.map_one of_subtype
id   └──────────────────┘ └────────┘
src  └──────────────────┘ └────────┘
typ  └──────────────────┘ └────────┘
doc  └──────────────────┘
 40  
 41  lemma eq_inv_iff_eq {f : perm α} {x y : α} : x = f⁻¹ y ↔ f x = y :=
id                            └──┘                └┘      
src                           └──┘                    └┘        
typ                           └──┘                └┘      
doc                           └──┘
 42  by conv {to_lhs, rw [← injective.eq_iff f.injective, apply_inv_self]}
id                          └──────────────┘ └─────────┘  └────────────┘
src     └────┘└────┘└┘└────┘└──────────────┘└─────────┘└┘└────────────┘└─
typ     └────┘└────┘└┘└────┘└──────────────┘└─────────┘└┘└────────────┘└─
txt     └────┘└────┘└┘└────┘                           └┘              └─
par     └────┘└────┘└┘└────┘                           └┘              └─
pid         └─────────────┘                           └┘              └┘
st     └─────┘└────┘└──────────────────────────────────┘└──────────────┘ 
 43  
src  
typ  
txt  
par  
pid  
st   
 44  lemma inv_eq_iff_eq {f : perm α} {x y : α} : f⁻¹ x = y ↔ x = f y :=
id                            └──┘              └┘        
src                           └──┘                 └┘         
typ                           └──┘              └┘        
doc                           └──┘
 45  by rw [eq_comm, eq_inv_iff_eq, eq_comm]
id          └─────┘  └───────────┘  └─────┘
src     └──┘└─────┘└┘└───────────┘└┘└─────┘└─
typ     └──┘└─────┘└┘└───────────┘└┘└─────┘└─
doc     └──┘       └┘             └┘       └─
txt     └──┘       └┘             └┘       └─
par     └──┘       └┘             └┘       └─
pid       └┘       └┘             └┘       
st     └──────────┘└─────────────┘└───────┘
 46  
src  
typ  
doc  
txt  
par  
pid  
st   
 47  def disjoint (f g : perm α) := ∀ x, f x = x ∨ g x = x
id                       └──┘                  
src                      └──┘                        
typ                      └──┘                  
doc                      └──┘
 48  
 49  @[symm] lemma disjoint.symm {f g : perm α} : disjoint f g → disjoint g f :=
id                                      └──┘     └──────┘     └──────┘  
src    └──┘                             └──┘      └──────┘       └──────┘
typ                                     └──┘     └──────┘     └──────┘  
doc    └──┘                             └──┘
 50  by simp [disjoint, or.comm]
id            └──────┘  └─────┘
src     └────┘└──────┘└┘└─────┘└─
typ     └────┘└──────┘└┘└─────┘└─
doc     └────┘        └┘       └─
txt     └────┘        └┘       └─
par     └────┘        └┘       └─
pid                 └┘       
st     └─────────────────────────
 51  
src  
typ  
doc  
txt  
par  
pid  
st   
 52  lemma disjoint_comm {f g : perm α} : disjoint f g ↔ disjoint g f :=
id                              └──┘     └──────┘    └──────┘  
src                             └──┘      └──────┘      └──────┘
typ                             └──┘     └──────┘    └──────┘  
doc                             └──┘
 53  ⟨disjoint.symm, disjoint.symm⟩
id    └───────────┘  └───────────┘
src   └───────────┘  └───────────┘
typ   └───────────┘  └───────────┘
 54  
 55  lemma disjoint_mul_comm {f g : perm α} (h : disjoint f g) : f * g = g * f :=
id                                  └──┘        └──────┘            
src                                 └──┘         └──────┘                
typ                                 └──┘        └──────┘            
doc                                 └──┘
 56  equiv.ext _ _ $ λ x, (h x).elim
id   └───────┘              └──┘
src  └───────┘                 └──┘
typ  └───────┘              └──┘
 57    (λ hf, (h (g x)).elim (λ hg, by simp [mul_apply, hf, hg])
id        └┘        └──┘     └┘           └───────┘  └┘  └┘
src                    └──┘            └────┘└───────┘└┘  └┘  
typ       └┘        └──┘     └┘     └────┘└───────┘└┘└┘└┘└┘
doc                                    └────┘         └┘  └┘  
txt                                    └────┘         └┘  └┘  
par                                    └────┘         └┘  └┘  
pid                                                 └┘  └┘  
st                                    └───────────────────────┘
 58      (λ hg, by simp [mul_apply, hf, g.injective hg]))
id          └┘           └───────┘  └┘  └─────────┘ └┘
src                └────┘└───────┘└┘  └┘└─────────┘  
typ         └┘     └────┘└───────┘└┘└┘└┘└─────────┘└┘
doc                └────┘         └┘  └┘             
txt                └────┘         └┘  └┘             
par                └────┘         └┘  └┘             
pid                             └┘  └┘             
st                └───────────────────────────────────┘
 59    (λ hg, (h (f x)).elim (λ hf, by simp [mul_apply, f.injective hf, hg])
id        └┘        └──┘     └┘           └───────┘  └─────────┘ └┘  └┘
src                    └──┘            └────┘└───────┘└┘└─────────┘  └┘  
typ       └┘        └──┘     └┘     └────┘└───────┘└┘└─────────┘└┘└┘└┘
doc                                    └────┘         └┘             └┘  
txt                                    └────┘         └┘             └┘  
par                                    └────┘         └┘             └┘  
pid                                                 └┘             └┘  
st                                    └───────────────────────────────────┘
 60      (λ hf, by simp [mul_apply, hf, hg]))
id          └┘           └───────┘  └┘  └┘
src                └────┘└───────┘└┘  └┘  
typ         └┘     └────┘└───────┘└┘└┘└┘└┘
doc                └────┘         └┘  └┘  
txt                └────┘         └┘  └┘  
par                └────┘         └┘  └┘  
pid                             └┘  └┘  
st                └───────────────────────┘
 61  
 62  @[simp] lemma disjoint_one_left (f : perm α) : disjoint 1 f := λ _, or.inl rfl
id                                        └──┘     └──────┘           └────┘ └─┘
src                                       └──┘      └──────┘             └────┘ └─┘
typ                                       └──┘     └──────┘           └────┘ └─┘
doc    └──┘                               └──┘
 63  
 64  @[simp] lemma disjoint_one_right (f : perm α) : disjoint f 1 := λ _, or.inr rfl
id                                         └──┘     └──────┘           └────┘ └─┘
src                                        └──┘      └──────┘             └────┘ └─┘
typ                                        └──┘     └──────┘           └────┘ └─┘
doc    └──┘                                └──┘
 65  
 66  lemma disjoint_mul_left {f g h : perm α} (H1 : disjoint f h) (H2 : disjoint g h) :
id                                    └──┘         └──────┘          └──────┘  
src                                   └──┘          └──────┘            └──────┘
typ                                   └──┘         └──────┘          └──────┘  
doc                                   └──┘
 67    disjoint (f * g) h :=
id     └──────┘      
src    └──────┘    
typ    └──────┘      
 68  λ x, by cases H1 x; cases H2 x; simp *
id                └┘         └┘ 
src          └────┘     └────┘     └──────
typ         └────┘└┘  └────┘└┘  └──────
doc          └────┘     └────┘     └──────
txt          └────┘     └────┘     └──────
par          └────┘     └────┘     └──────
pid                                  
st          └───────────────────────────────
 69  
src  
typ  
doc  
txt  
par  
pid  
st   
 70  lemma disjoint_mul_right {f g h : perm α} (H1 : disjoint f g) (H2 : disjoint f h) :
id                                     └──┘         └──────┘          └──────┘  
src                                    └──┘          └──────┘            └──────┘
typ                                    └──┘         └──────┘          └──────┘  
doc                                    └──┘
 71    disjoint f (g * h) :=
id     └──────┘     
src    └──────┘      
typ    └──────┘     
 72  by rw disjoint_comm; exact disjoint_mul_left H1.symm H2.symm
id         └───────────┘        └───────────────┘ └─────┘ └─────┘
src     └─┘└───────────┘  └────┘└───────────────┘└─────┘└─────┘
typ     └─┘└───────────┘  └────┘└───────────────┘└─────┘└─────┘
doc     └─┘               └────┘                               
txt     └─┘               └────┘                               
par     └─┘               └────┘                               
pid                                                          
st     └──────────────────────────────────────────────────────────
 73  
src  
typ  
doc  
txt  
par  
pid  
st   
 74  lemma disjoint_prod_right {f : perm α} (l : list (perm α))
id                                  └──┘        └──┘  └──┘ 
src                                 └──┘         └──┘  └──┘
typ                                 └──┘        └──┘  └──┘ 
doc                                 └──┘               └──┘
 75    (h : ∀ g ∈ l, disjoint f g) : disjoint f l.prod :=
id                 └──────┘      └──────┘  └───┘
src                 └──────┘        └──────┘    └───┘
typ                └──────┘      └──────┘  └───┘
doc                                              └───┘
 76  begin
st   └─────
 77    induction l with g l ih,
id               
src    └────────┘ └──────────┘
typ    └────────┘└──────────┘
doc    └────────┘ └──────────┘
txt    └────────┘ └──────────┘
par    └────────┘ └──────────┘
pid              └─────────┘
st   ────────────────────────┘└─
 78    { exact disjoint_one_right _ },
id             └────────────────┘
src      └────┘└────────────────┘└─┘
typ      └────┘└────────────────┘└─┘
doc      └────┘                  └─┘
txt      └────┘                  └─┘
par      └────┘                  └─┘
pid                             └┘
st   ───┘└─────────────────────────┘└┘
 79    { rw list.prod_cons;
id          └────────────┘
src      └─┘└────────────┘
typ      └─┘└────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────────────
 80      exact disjoint_mul_right (h _ (list.mem_cons_self _ _))
id             └────────────────┘       └────────────────┘
src      └────┘└────────────────┘  └─┘ └────────────────┘└──────
typ      └────┘└────────────────┘  └─┘ └────────────────┘└──────
doc      └────┘                    └─┘                   └──────
txt      └────┘                    └─┘                   └──────
par      └────┘                    └─┘                   └──────
pid                               └─┘                   └──────
st   ────────────────────────────────────────────────────────────
 81        (ih (λ g hg, h g (list.mem_cons_of_mem _ hg))) }
id          └┘              └──────────────────┘
src  ─────┘     └─────┘   └──────────────────┘└─┘  └──┘
typ  ─────┘ └┘  └─────┘  └──────────────────┘└─┘  └──┘
doc  ─────┘     └─────┘                       └─┘  └──┘
txt  ─────┘     └─────┘                       └─┘  └──┘
par  ─────┘     └─────┘                       └─┘  └──┘
pid  ─────┘     └─────┘                       └─┘  └─┘
st   ────────────────────────────────────────────────────┘└─
 82  end
st   ──┘
 83  
 84  lemma disjoint_prod_perm {l₁ l₂ : list (perm α)} (hl : l₁.pairwise disjoint)
id                                     └──┘  └──┘          └┘└───────┘ └──────┘
src                                    └──┘  └──┘             └───────┘ └──────┘
typ                                    └──┘  └──┘          └┘└───────┘ └──────┘
doc                                          └──┘             └───────┘
 85    (hp : l₁ ~ l₂) : l₁.prod = l₂.prod :=
id           └┘  └┘    └┘└───┘  └┘└───┘
src                      └───┘    └───┘
typ          └┘  └┘    └┘└───┘  └┘└───┘
doc                      └───┘     └───┘
 86  begin
st   └─────
 87    induction hp,
id               └┘
src    └────────┘
typ    └────────┘└┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ─────────────┘└─
 88    { refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
 89    { rw [list.prod_cons, list.prod_cons, hp_ih (list.pairwise_cons.1 hl).2] },
id           └────────────┘  └────────────┘  └───┘  └────────────────┘   └┘
src      └──┘└────────────┘└┘└────────────┘└┘      └────────────────┘└─┘  └───┘
typ      └──┘└────────────┘└┘└────────────┘└┘└───┘ └────────────────┘└─┘└┘└───┘
doc      └──┘              └┘              └┘                        └─┘  └───┘
txt      └──┘              └┘              └┘                        └─┘  └───┘
par      └──┘              └┘              └┘                        └─┘  └───┘
pid        └┘              └┘              └┘                        └─┘  └──┘
st   ───┘└────────────────┘└──────────────┘└───────────────────────────────┘└─┘└┘
 90    { simp [list.prod_cons, disjoint_mul_comm, (mul_assoc _ _ _).symm, *,
id             └────────────┘  └───────────────┘   └───────┘
src      └────┘└────────────┘└┘└───────────────┘└┘ └───────┘└────────────────
typ      └────┘└────────────┘└┘└───────────────┘└┘ └───────┘└────────────────
doc      └────┘              └┘                 └┘          └────────────────
txt      └────┘              └┘                 └┘          └────────────────
par      └────┘              └┘                 └┘          └────────────────
pid                        └┘                 └┘          └────────────────
st   ───┘└───────────────────────────────────────────────────────────────────
 91        list.pairwise_cons] at * },
id         └────────────────┘
src  ─────┘└────────────────┘└─────┘
typ  ─────┘└────────────────┘└─────┘
doc  ─────┘                  └─────┘
txt  ─────┘                  └─────┘
par  ─────┘                  └─────┘
pid  ─────┘                  └──┘
st   ──────────────────────────────┘└┘
 92    { rw [hp_ih_a hl, hp_ih_a_1 ((list.perm_pairwise (λ x y (h : disjoint x y), disjoint.symm h) hp_a).1 hl)] }
id           └─────┘ └┘  └───────┘   └────────────────┘             └──────┘       └───────────┘    └──┘    └┘
src      └──┘         └┘           └────────────────┘  └────────┘└──────┘  └─┘└───────────┘ └┘    └──┘  └─┘
typ      └──┘└─────┘└┘└┘└───────┘  └────────────────┘  └────────┘└──────┘  └─┘└───────────┘ └┘└──┘└──┘└┘└─┘
doc      └──┘         └┘                               └────────┘          └─┘              └┘    └──┘  └─┘
txt      └──┘         └┘                               └────────┘          └─┘              └┘    └──┘  └─┘
par      └──┘         └┘                               └────────┘          └─┘              └┘    └──┘  └─┘
pid        └┘         └┘                               └────────┘          └─┘              └┘    └──┘  └┘
st   ─────────────────┘└──────────────────────────────────────────────────────────────────────────────────────┘└─
 93  end
st   ──┘
 94  
 95  lemma of_subtype_subtype_perm {f : perm α} {p : α → Prop} [decidable_pred p] (h₁ : ∀ x, p x ↔ p (f x))
id                                      └──┘                  └────────────┘                   
src                                     └──┘                    └────────────┘                   
typ                                     └──┘                  └────────────┘                   
doc                                     └──┘
 96    (h₂ : ∀ x, f x ≠ x → p x) : of_subtype (subtype_perm f h₁) = f :=
id                          └────────┘  └──────────┘  └┘   
src                               └────────┘  └──────────┘       
typ                         └────────┘  └──────────┘  └┘   
 97  equiv.ext _ _ $ λ x, begin
id   └───────┘         
src  └───────┘
typ  └───────┘         
st                        └─────
 98    rw [of_subtype, subtype_perm],
id         └────────┘  └──────────┘
src    └──┘└────────┘└┘└──────────┘
typ    └──┘└────────┘└┘└──────────┘
doc    └──┘          └┘            
txt    └──┘          └┘            
par    └──┘          └┘            
pid      └┘          └┘            
st   ───────────────┘└────────────┘└──
 99    by_cases hx : p x,
id                    
src    └───────┘  └─┘ 
typ    └───────┘  └─┘
doc    └───────┘  └─┘ 
txt    └───────┘  └─┘ 
par    └───────┘  └─┘ 
pid              └─┘ 
st   ──────────────────┘└─
100    { simp [hx] },
id             └┘
src      └────┘  └┘
typ      └────┘└┘└┘
doc      └────┘  └┘
txt      └────┘  └┘
par      └────┘  └┘
pid            
st   ───┘└────────┘└┘
101    { haveI := classical.prop_decidable,
id                └──────────────────────┘
src      └───────┘└──────────────────────┘
typ      └───────┘└──────────────────────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
pid           └─┘
st   ────────────────────────────────────┘└─
102      simp [hx, not_not.1 (mt (h₂ x) hx)] }
id             └┘  └─────┘    └┘  └┘   └┘
src      └────┘  └┘└─────┘└─┘ └┘    └┘  └─┘
typ      └────┘└┘└┘└─────┘└─┘ └┘ └┘└┘└┘└─┘
doc      └────┘  └┘       └─┘       └┘  └─┘
txt      └────┘  └┘       └─┘       └┘  └─┘
par      └────┘  └┘       └─┘       └┘  └─┘
pid            └┘       └─┘       └┘  └┘
st   ───────────────────────────────────────┘└─
103  end
st   ──┘
104  
105  lemma of_subtype_apply_of_not_mem {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) {x : α} (hx : ¬ p x) :
id                                                    └────────────┘        └──┘  └─────┘                   
src                                                    └────────────┘         └──┘  └─────┘                   
typ                                                   └────────────┘        └──┘  └─────┘                   
doc                                                                           └──┘
106    of_subtype f x = x := dif_neg hx
id     └────────┘        └─────┘ └┘
src    └────────┘           └─────┘
typ    └────────┘        └─────┘ └┘
107  
108  lemma mem_iff_of_subtype_apply_mem {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) (x : α) :
id                                                     └────────────┘        └──┘  └─────┘         
src                                                     └────────────┘         └──┘  └─────┘
typ                                                    └────────────┘        └──┘  └─────┘         
doc                                                                            └──┘
109    p x ↔ p ((of_subtype f : α → α) x) :=
id           └────────┘         
src             └────────┘
typ          └────────┘         
110  if h : p x then by dsimp [of_subtype]; simpa [h] using (f ⟨x, h⟩).2
id   └┘                      └────────┘                       
src  └┘                 └─────┘└────────┘  └─────┘ └──────┘    └┘ └───┘
typ  └┘               └─────┘└────────┘  └─────┘└──────┘  └┘└───┘
doc                     └─────┘            └─────┘ └──────┘    └┘ └───┘
txt                     └─────┘            └─────┘ └──────┘    └┘ └───┘
par                     └─────┘            └─────┘ └──────┘    └┘ └───┘
pid                                            └────┘    └┘ └┘└─┘
st                     └────────────────────────────────────────────────┘
111  else by simp [h, of_subtype_apply_of_not_mem f h]
id                   └─────────────────────────┘  
src          └────┘ └┘└─────────────────────────┘  └─
typ          └────┘└┘└─────────────────────────┘└─
doc          └────┘ └┘                             └─
txt          └────┘ └┘                             └─
par          └────┘ └┘                             └─
pid               └┘                             
st          └──────────────────────────────────────────
112  
src  
typ  
doc  
txt  
par  
pid  
st   
113  @[simp] lemma subtype_perm_of_subtype {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) :
id                                                        └────────────┘        └──┘  └─────┘ 
src                                                        └────────────┘         └──┘  └─────┘
typ                                                       └────────────┘        └──┘  └─────┘ 
doc    └──┘                                                                       └──┘
114    subtype_perm (of_subtype f) (mem_iff_of_subtype_apply_mem f) = f :=
id     └──────────┘  └────────┘    └──────────────────────────┘    
src    └──────────┘  └────────┘     └──────────────────────────┘    
typ    └──────────┘  └────────┘    └──────────────────────────┘    
115  equiv.ext _ _ $ λ ⟨x, hx⟩, by dsimp [subtype_perm, of_subtype]; simp [show p x, from hx]
id   └───────┘                           └──────────┘  └────────┘                      └┘
src  └───────┘                     └─────┘└──────────┘└┘└────────┘  └────┘      └─────┘  └─
typ  └───────┘                    └─────┘└──────────┘└┘└────────┘  └────┘    └─────┘└┘└─
doc                                └─────┘            └┘            └────┘      └─────┘  └─
txt                                └─────┘            └┘            └────┘      └─────┘  └─
par                                └─────┘            └┘            └────┘      └─────┘  └─
pid                                                 └┘                      └─────┘  
st                                └───────────────────────────────────────────────────────────
116  
src  
typ  
doc  
txt  
par  
pid  
st   
117  lemma pow_apply_eq_self_of_apply_eq_self {f : perm α} {x : α} (hfx : f x = x) :
id                                                 └──┘                    
src                                                └──┘                       
typ                                                └──┘                    
doc                                                └──┘
118    ∀ n : ℕ, (f ^ n) x = x
id                   
src                     
typ                  
119  | 0     := rfl
id              └─┘
src             └─┘
typ             └─┘
120  | (n+1) := by rw [pow_succ', mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self]
id                    └───────┘  └───────┘  └─┘  └────────────────────────────────┘
src               └──┘└───────┘└┘└───────┘└┘   └┘                                  └─
typ               └──┘└───────┘└┘└───────┘└┘└─┘└┘└────────────────────────────────┘└─
doc                └──┘         └┘         └┘   └┘                                  └─
txt                └──┘         └┘         └┘   └┘                                  └─
par                └──┘         └┘         └┘   └┘                                  └─
pid                  └┘         └┘         └┘   └┘                                  
st                └────────────┘└─────────┘└───┘└──────────────────────────────────┘
121  
src  
typ  
doc  
txt  
par  
pid  
st   
122  lemma gpow_apply_eq_self_of_apply_eq_self {f : perm α} {x : α} (hfx : f x = x) :
id                                                  └──┘                    
src                                                 └──┘                       
typ                                                 └──┘                    
doc                                                 └──┘
123    ∀ n : ℤ, (f ^ n) x = x
id                   
src                     
typ                  
124  | (n : ℕ) := pow_apply_eq_self_of_apply_eq_self hfx n
id              └────────────────────────────────┘ └─┘
src              └────────────────────────────────┘
typ             └────────────────────────────────┘ └─┘
125  | -[1+ n] := by rw [gpow_neg_succ, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]
id     └──┘             └───────────┘  └───────────┘  └────────────────────────────────┘ └─┘
src    └──┘         └──┘└───────────┘└┘└───────────┘└┘└────────────────────────────────┘   └─
typ    └──┘         └──┘└───────────┘└┘└───────────┘└┘└────────────────────────────────┘└─┘└─
doc                  └──┘             └┘             └┘                                     └─
txt                  └──┘             └┘             └┘                                     └─
par                  └──┘             └┘             └┘                                     └─
pid                    └┘             └┘             └┘                                     
st                  └────────────────┘└─────────────┘└──────────────────────────────────────┘
126  
src  
typ  
doc  
txt  
par  
pid  
st   
127  lemma pow_apply_eq_of_apply_apply_eq_self {f : perm α} {x : α} (hffx : f (f x) = x) :
id                                                  └──┘                        
src                                                 └──┘                            
typ                                                 └──┘                        
doc                                                 └──┘
128    ∀ n : ℕ, (f ^ n) x = x ∨ (f ^ n) x = f x
id                             
src                                  
typ                            
129  | 0     := or.inl rfl
id              └────┘ └─┘
src             └────┘ └─┘
typ             └────┘ └─┘
130  | (n+1) := (pow_apply_eq_of_apply_apply_eq_self n).elim
id             └─────────────────────────────────┘   └──┘
src                                                   └──┘
typ            └─────────────────────────────────┘   └──┘
131    (λ h, or.inr (by rw [pow_succ, mul_apply, h]))
id          └────┘         └──────┘  └───────┘  
src          └────┘     └──┘└──────┘└┘└───────┘└┘ 
typ         └────┘     └──┘└──────┘└┘└───────┘└┘
doc                     └──┘        └┘         └┘ 
txt                     └──┘        └┘         └┘ 
par                     └──┘        └┘         └┘ 
pid                       └┘        └┘         └┘ 
st                     └───────────┘└─────────┘└─┘
132    (λ h, or.inl (by rw [pow_succ, mul_apply, h, hffx]))
id          └────┘         └──────┘  └───────┘    └──┘
src          └────┘     └──┘└──────┘└┘└───────┘└┘ └┘    
typ         └────┘     └──┘└──────┘└┘└───────┘└┘└┘└──┘
doc                     └──┘        └┘         └┘ └┘    
txt                     └──┘        └┘         └┘ └┘    
par                     └──┘        └┘         └┘ └┘    
pid                       └┘        └┘         └┘ └┘    
st                     └───────────┘└─────────┘└─┘└────┘
133  
134  lemma gpow_apply_eq_of_apply_apply_eq_self {f : perm α} {x : α} (hffx : f (f x) = x) :
id                                                   └──┘                        
src                                                  └──┘                            
typ                                                  └──┘                        
doc                                                  └──┘
135    ∀ i : ℤ, (f ^ i) x = x ∨ (f ^ i) x = f x
id                             
src                                  
typ                            
136  | (n : ℕ) := pow_apply_eq_of_apply_apply_eq_self hffx n
id              └─────────────────────────────────┘ └──┘
src              └─────────────────────────────────┘
typ             └─────────────────────────────────┘ └──┘
137  | -[1+ n] :=
id     └──┘  
src    └──┘  
typ    └──┘  
138    by rw [gpow_neg_succ, inv_eq_iff_eq, ← injective.eq_iff f.injective, ← mul_apply, ← pow_succ,
id            └───────────┘  └───────────┘    └──────────────┘ └─────────┘    └───────┘    └──────┘
src       └──┘└───────────┘└┘└───────────┘└──┘└──────────────┘└─────────┘└──┘└───────┘└──┘└──────┘└─
typ       └──┘└───────────┘└┘└───────────┘└──┘└──────────────┘└─────────┘└──┘└───────┘└──┘└──────┘└─
doc       └──┘             └┘             └──┘                           └──┘         └──┘        └─
txt       └──┘             └┘             └──┘                           └──┘         └──┘        └─
par       └──┘             └┘             └──┘                           └──┘         └──┘        └─
pid         └┘             └┘             └──┘                           └──┘         └──┘        └─
st       └────────────────┘└─────────────┘└──────────────────────────────┘└───────────┘└──────────┘└─
139      eq_comm, inv_eq_iff_eq, ← mul_apply, ← pow_succ', @eq_comm _ x, or.comm];
id       └─────┘  └───────────┘    └───────┘    └───────┘   └─────┘     └─────┘
src  ───┘└─────┘└┘└───────────┘└──┘└───────┘└──┘└───────┘└┘ └─────┘└─┘ └┘└─────┘
typ  ───┘└─────┘└┘└───────────┘└──┘└───────┘└──┘└───────┘└┘ └─────┘└─┘└┘└─────┘
doc  ───┘       └┘             └──┘         └──┘         └┘        └─┘ └┘       
txt  ───┘       └┘             └──┘         └──┘         └┘        └─┘ └┘       
par  ───┘       └┘             └──┘         └──┘         └┘        └─┘ └┘       
pid  ───┘       └┘             └──┘         └──┘         └┘        └─┘ └┘       
st   ──────────┘└─────────────┘└───────────┘└───────────┘└────────────┘└───────┘└─
140    exact pow_apply_eq_of_apply_apply_eq_self hffx _
id           └─────────────────────────────────┘ └──┘
src    └────┘└─────────────────────────────────┘    └──
typ    └────┘└─────────────────────────────────┘└──┘└──
doc    └────┘                                       └──
txt    └────┘                                       └──
par    └────┘                                       └──
pid                                                └┘
st   ───────────────────────────────────────────────────
141  
src  
typ  
doc  
txt  
par  
pid  
st   
142  variable [decidable_eq α]
id             └──────────┘
src            └──────────┘
typ            └──────────┘
143  
144  def support [fintype α] (f : perm α) := univ.filter (λ x, f x ≠ x)
id                └─────┘        └──┘      └──┘└─────┘         
src               └─────┘         └──┘       └──┘└─────┘           
typ               └─────┘        └──┘      └──┘└─────┘         
doc               └─────┘         └──┘       └──┘└─────┘
145  
146  @[simp] lemma mem_support [fintype α] {f : perm α} {x : α} : x ∈ f.support ↔ f x ≠ x :=
id                              └─────┘        └──┘              └──────┘     
src                             └─────┘         └──┘                  └──────┘      
typ                             └─────┘        └──┘              └──────┘     
doc    └──┘                     └─────┘         └──┘
147  by simp [support]
id            └─────┘
src     └────┘└─────┘└─
typ     └────┘└─────┘└─
doc     └────┘       └─
txt     └────┘       └─
par     └────┘       └─
pid                
st     └───────────────
148  
src  
typ  
doc  
txt  
par  
pid  
st   
149  def is_swap (f : perm α) := ∃ x y, x ≠ y ∧ f = swap x y
id                    └──┘               └──┘  
src                   └──┘                     └──┘
typ                   └──┘               └──┘  
doc                   └──┘                          └──┘
150  
151  lemma swap_mul_eq_mul_swap (f : perm α) (x y : α) : swap x y * f = f * swap (f⁻¹ x) (f⁻¹ y) :=
id                                   └──┘              └──┘        └──┘  └┘    └┘ 
src                                  └──┘                └──┘            └──┘   └┘      └┘
typ                                  └──┘              └──┘        └──┘  └┘    └┘ 
doc                                  └──┘                └──┘               └──┘
152  equiv.ext _ _ $ λ z, begin
id   └───────┘         
src  └───────┘
typ  └───────┘         
st                        └─────
153    simp [mul_apply, swap_apply_def],
id           └───────┘  └────────────┘
src    └────┘└───────┘└┘└────────────┘
typ    └────┘└───────┘└┘└────────────┘
doc    └────┘         └┘              
txt    └────┘         └┘              
par    └────┘         └┘              
pid                 └┘              
st   ─────────────────────────────────┘└─
154    split_ifs;
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ─────────────
155    simp [*, eq_inv_iff_eq] at * <|> cc
id              └───────────┘
src    └───────┘└───────────┘└─────┘    └─┘
typ    └───────┘└───────────┘└─────┘    └─┘
doc    └───────┘             └─────┘    └─┘
txt    └───────┘             └─────┘    └─┘
par    └───────┘             └─────┘    └─┘
pid        └──┘             └──┘      
st   ─────────────────────────────────────┘
156  end
st   └─┘
157  
158  lemma mul_swap_eq_swap_mul (f : perm α) (x y : α) : f * swap x y = swap (f x) (f y) * f :=
id                                   └──┘                └──┘    └──┘          
src                                  └──┘                   └──┘      └──┘             
typ                                  └──┘                └──┘    └──┘          
doc                                  └──┘                    └──┘       └──┘
159  by rw [swap_mul_eq_mul_swap, inv_apply_self, inv_apply_self]
id          └──────────────────┘  └────────────┘  └────────────┘
src     └──┘└──────────────────┘└┘└────────────┘└┘└────────────┘└─
typ     └──┘└──────────────────┘└┘└────────────┘└┘└────────────┘└─
doc     └──┘                    └┘              └┘              └─
txt     └──┘                    └┘              └┘              └─
par     └──┘                    └┘              └┘              └─
pid       └┘                    └┘              └┘              
st     └───────────────────────┘└──────────────┘└──────────────┘
160  
src  
typ  
doc  
txt  
par  
pid  
st   
161  @[simp] lemma swap_mul_self (i j : α) : equiv.swap i j * equiv.swap i j = 1 :=
id                                          └────────┘    └────────┘   
src                                          └────────┘      └────────┘     
typ                                         └────────┘    └────────┘   
doc    └──┘                                  └────────┘       └────────┘
162  equiv.swap_swap i j
id   └─────────────┘  
src  └─────────────┘
typ  └─────────────┘  
163  
164  /-- Multiplying a permutation with `swap i j` twice gives the original permutation.
165  
166    This specialization of `swap_mul_self` is useful when using cosets of permutations.
167  -/
168  @[simp]
doc    └──┘
169  lemma swap_mul_self_mul (i j : α) (σ : perm α) : equiv.swap i j * (equiv.swap i j * σ) = σ :=
id                                         └──┘     └────────┘     └────────┘       
src                                         └──┘      └────────┘       └────────┘         
typ                                        └──┘     └────────┘     └────────┘       
doc                                         └──┘      └────────┘        └────────┘
170  by rw [←mul_assoc (swap i j) (swap i j) σ, equiv.perm.swap_mul_self, one_mul]
id           └───────┘             └──┘      └──────────────────────┘  └─────┘
src     └───┘└───────┘       └┘ └──┘  └┘ └┘└──────────────────────┘└┘└─────┘└─
typ     └───┘└───────┘       └┘ └──┘└┘└┘└──────────────────────┘└┘└─────┘└─
doc     └───┘                └┘ └──┘  └┘ └┘                        └┘       └─
txt     └───┘                └┘       └┘ └┘                        └┘       └─
par     └───┘                └┘       └┘ └┘                        └┘       └─
pid       └─┘                └┘       └┘ └┘                        └┘       
st     └─────────────────────────────────────┘└────────────────────────┘└───────┘
171  
src  
typ  
doc  
txt  
par  
pid  
st   
172  lemma swap_mul_eq_iff {i j : α} {σ : perm α} : swap i j * σ = σ ↔ i = j :=
id                                       └──┘     └──┘          
src                                       └──┘      └──┘              
typ                                      └──┘     └──┘          
doc                                       └──┘      └──┘
173  ⟨(assume h, have swap_id : swap i j = 1 := mul_right_cancel (trans h (one_mul σ).symm),
id                             └──┘         └──────────────┘  └───┘   └─────┘  └──┘
src                             └──┘           └──────────────┘  └───┘    └─────┘   └──┘
typ                            └──┘         └──────────────┘  └───┘   └─────┘  └──┘
doc                             └──┘
174    by {rw [←swap_apply_right i j, swap_id], refl}),
id              └──────────────┘    └─────┘
src        └───┘└──────────────┘  └┘         └──┘
typ        └───┘└──────────────┘└┘└─────┘  └──┘
doc        └───┘                  └┘         └──┘
txt        └───┘                  └┘         └──┘
par        └───┘                  └┘         └──┘
pid          └─┘                  └┘       
st       └─────────────────────────┘└───────┘└─────┘└┘
175  (assume h, by erw [h, swap_self, one_mul])⟩
id                       └───────┘  └─────┘
src                └───┘ └┘└───────┘└┘└─────┘
typ               └───┘└┘└───────┘└┘└─────┘
doc                └───┘ └┘         └┘       
txt                └───┘ └┘         └┘       
par                └───┘ └┘         └┘       
pid                   └┘ └┘         └┘       
st                └─────┘└─────────┘└───────┘
176  
177  @[simp] lemma swap_swap_apply (i j k : α) : equiv.swap i j (equiv.swap i j k) = k :=
id                                              └────────┘    └────────┘      
src                                              └────────┘      └────────┘        
typ                                             └────────┘    └────────┘      
doc    └──┘                                      └────────┘      └────────┘
178  equiv.swap_core_swap_core k i j
id   └───────────────────────┘   
src  └───────────────────────┘
typ  └───────────────────────┘   
179  
180  lemma is_swap_of_subtype {p : α → Prop} [decidable_pred p]
id                                           └────────────┘ 
src                                           └────────────┘
typ                                          └────────────┘ 
181    {f : perm (subtype p)} (h : is_swap f) : is_swap (of_subtype f) :=
id          └──┘  └─────┘         └─────┘     └─────┘  └────────┘ 
src         └──┘  └─────┘          └─────┘      └─────┘  └────────┘
typ         └──┘  └─────┘         └─────┘     └─────┘  └────────┘ 
doc         └──┘
182  let ⟨⟨x, hx⟩, ⟨y, hy⟩, hxy⟩ := h in
id   └─┘                          
typ  └─┘                          
183  ⟨x, y, by simp at hxy; tauto,
src            └─────────┘  └───┘
typ            └─────────┘  └───┘
doc            └─────────┘  └───┘
txt            └─────────┘  └───┘
par            └─────────┘  └───┘
pid                └────┘
st            └─────────────────┘
184    equiv.ext _ _ $ λ z, begin
id     └───────┘         
src    └───────┘
typ    └───────┘         
st                          └─────
185      rw [hxy.2, of_subtype],
id           └─┘    └────────┘
src      └──┘   └──┘└────────┘
typ      └──┘└─┘└──┘└────────┘
doc      └──┘   └──┘          
txt      └──┘   └──┘          
par      └──┘   └──┘          
pid        └┘   └──┘          
st   ──────────┘└────────────┘└──
186      simp [swap_apply_def],
id             └────────────┘
src      └────┘└────────────┘
typ      └────┘└────────────┘
doc      └────┘              
txt      └────┘              
par      └────┘              
pid                        
st   ────────────────────────┘└─
187      split_ifs;
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
st   ───────────────
188      cc <|> simp * at *
src      └─┘    └───────────
typ      └─┘    └───────────
doc      └─┘    └───────────
txt      └─┘    └───────────
par      └─┘    └───────────
pid                └──┘
st   ───────────────────────
189    end⟩
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
190  
191  lemma ne_and_ne_of_swap_mul_apply_ne_self {f : perm α} {x y : α}
id                                                  └──┘          
src                                                 └──┘
typ                                                 └──┘          
doc                                                 └──┘
192    (hy : (swap x (f x) * f) y ≠ y) : f y ≠ y ∧ y ≠ x :=
id            └──┘                      
src           └──┘                               
typ           └──┘                      
doc           └──┘
193  begin
st   └─────
194    simp only [swap_apply_def, mul_apply, injective.eq_iff f.injective] at *,
id                └────────────┘  └───────┘  └──────────────┘ └─────────┘
src    └─────────┘└────────────┘└┘└───────┘└┘└──────────────┘└─────────┘└────┘
typ    └─────────┘└────────────┘└┘└───────┘└┘└──────────────┘└─────────┘└────┘
doc    └─────────┘              └┘         └┘                           └────┘
txt    └─────────┘              └┘         └┘                           └────┘
par    └─────────┘              └┘         └┘                           └────┘
pid        └──┘└┘              └┘         └┘                           └──┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
195    by_cases h : f y = x,
id                     
src    └───────┘ └─┘  
typ    └───────┘ └─┘
doc    └───────┘ └─┘   
txt    └───────┘ └─┘   
par    └───────┘ └─┘   
pid             └─┘   
st   ─────────────────────┘└─
196    { split; intro; simp * at * },
src      └───┘  └───┘  └──────────┘
typ      └───┘  └───┘  └──────────┘
doc      └───┘  └───┘  └──────────┘
txt      └───┘  └───┘  └──────────┘
par      └───┘  └───┘  └──────────┘
pid                        └──┘
st   ───┘└────────────────────────┘└┘
197    { split_ifs at hy; cc }
src      └─────────────┘  └─┘
typ      └─────────────┘  └─┘
doc      └─────────────┘  └─┘
txt      └─────────────┘  └─┘
par      └─────────────┘  └─┘
pid               └────┘    
st   ───────────────────────┘└─
198  end
st   ──┘
199  
200  lemma support_swap_mul_eq [fintype α] {f : perm α} {x : α}
id                              └─────┘        └──┘        
src                             └─────┘         └──┘
typ                             └─────┘        └──┘        
doc                             └─────┘         └──┘
201    (hffx : f (f x) ≠ x) : (swap x (f x) * f).support = f.support.erase x :=
id                        └──┘        └─────┘   └──────┘└────┘ 
src                           └──┘            └─────┘    └──────┘└────┘
typ                       └──┘        └─────┘   └──────┘└────┘ 
doc                            └──┘                                 └────┘
202  have hfx : f x ≠ x, from λ hfx, by simpa [hfx] using hffx,
id                          └─┘            └─┘        └──┘
src                                    └─────┘   └──────┘
typ                         └─┘     └─────┘└─┘└──────┘└──┘
doc                                     └─────┘   └──────┘
txt                                     └─────┘   └──────┘
par                                     └─────┘   └──────┘
pid                                             └────┘
st                                     └─────────────────────┘
203  finset.ext.2 $ λ y,
id   └────────┘      
src  └────────┘
typ  └────────┘      
204  ⟨λ hy, have hy' : (swap x (f x) * f) y ≠ y, from mem_support.1 hy,
id      └┘              └──┘                  └─────────┘  └┘
src                     └──┘                        └─────────┘
typ     └┘              └──┘                  └─────────┘  └┘
doc                     └──┘
205      mem_erase.2 ⟨λ hyx, by simp [hyx, mul_apply, *] at *,
id       └───────┘     └─┘           └─┘  └───────┘
src      └───────┘             └────┘   └┘└───────┘└───────┘
typ      └───────┘     └─┘     └────┘└─┘└┘└───────┘└───────┘
doc                             └────┘   └┘         └───────┘
txt                             └────┘   └┘         └───────┘
par                             └────┘   └┘         └───────┘
pid                                    └┘         └──┘└──┘
st                             └────────────────────────────┘
206      mem_support.2 $ λ hfy,
id       └─────────┘      └─┘
src      └─────────┘
typ      └─────────┘      └─┘
207        by simp only [mul_apply, swap_apply_def, hfy] at hy';
id                       └───────┘  └────────────┘  └─┘
src           └─────────┘└───────┘└┘└────────────┘└┘   └──────┘
typ           └─────────┘└───────┘└┘└────────────┘└┘└─┘└──────┘
doc           └─────────┘         └┘              └┘   └──────┘
txt           └─────────┘         └┘              └┘   └──────┘
par           └─────────┘         └┘              └┘   └──────┘
pid               └──┘└┘         └┘              └┘   └────┘
st           └───────────────────────────────────────────────────
208        split_ifs at hy'; simp * at *⟩,
src        └──────────────┘  └─────────┘
typ        └──────────────┘  └─────────┘
doc        └──────────────┘  └─────────┘
txt        └──────────────┘  └─────────┘
par        └──────────────┘  └─────────┘
pid                 └─────┘      └──┘
st   ──────────────────────────────────┘
209    λ hy, by simp only [mem_erase, mem_support, swap_apply_def, mul_apply] at *;
id       └┘                └───────┘  └─────────┘  └────────────┘  └───────┘
src             └─────────┘└───────┘└┘└─────────┘└┘└────────────┘└┘└───────┘└────┘
typ      └┘     └─────────┘└───────┘└┘└─────────┘└┘└────────────┘└┘└───────┘└────┘
doc             └─────────┘         └┘           └┘              └┘         └────┘
txt             └─────────┘         └┘           └┘              └┘         └────┘
par             └─────────┘         └┘           └┘              └┘         └────┘
pid                 └──┘└┘         └┘           └┘              └┘         └──┘
st             └────────────────────────────────────────────────────────────────────
210      intro; split_ifs at *; simp * at *⟩
src      └───┘  └────────────┘  └─────────┘
typ      └───┘  └────────────┘  └─────────┘
doc      └───┘  └────────────┘  └─────────┘
txt      └───┘  └────────────┘  └─────────┘
par      └───┘  └────────────┘  └─────────┘
pid                      └───┘      └──┘
st   ─────────────────────────────────────┘
211  
212  lemma card_support_swap_mul [fintype α] {f : perm α} {x : α}
id                                └─────┘        └──┘        
src                               └─────┘         └──┘
typ                               └─────┘        └──┘        
doc                               └─────┘         └──┘
213    (hx : f x ≠ x) : (swap x (f x) * f).support.card < f.support.card :=
id                   └──┘        └─────┘ └──┘   └──────┘└───┘
src                     └──┘            └─────┘ └──┘    └──────┘└───┘
typ                  └──┘        └─────┘ └──┘   └──────┘└───┘
doc                      └──┘                     └──┘             └───┘
214  finset.card_lt_card
id   └─────────────────┘
src  └─────────────────┘
typ  └─────────────────┘
215    ⟨λ z hz, mem_support.2 (ne_and_ne_of_swap_mul_apply_ne_self (mem_support.1 hz)).1,
id         └┘  └─────────┘   └─────────────────────────────────┘  └─────────┘  └┘  
src             └─────────┘   └─────────────────────────────────┘  └─────────┘      
typ        └┘  └─────────┘   └─────────────────────────────────┘  └─────────┘  └┘  
216      λ h, absurd (h (mem_support.2 hx)) (mt mem_support.1 (by simp))⟩
id           └────┘    └─────────┘  └┘    └┘ └─────────┘
src           └────┘     └─────────┘        └┘ └─────────┘      └──┘
typ          └────┘    └─────────┘  └┘    └┘ └─────────┘      └──┘
doc                                                               └──┘
txt                                                               └──┘
par                                                               └──┘
st                                                               └───┘
217  
218  def swap_factors_aux : Π (l : list α) (f : perm α), (∀ {x}, f x ≠ x → x ∈ l) →
id                                └──┘        └──┘                  
src                                └──┘         └──┘                        
typ                               └──┘        └──┘                  
doc                                             └──┘
219    {l : list (perm α) // l.prod = f ∧ ∀ g ∈ l, is_swap g}
id         └──┘  └──┘      └───┘           └─────┘ 
src        └──┘  └──┘        └───┘              └─────┘
typ        └──┘  └──┘      └───┘           └─────┘ 
doc               └──┘        └───┘
220  | []       := λ f h, ⟨[], equiv.ext _ _ $ λ x, by rw [list.prod_nil];
id     └┘                └┘  └───────┘                  └───────────┘
src    └┘                  └┘  └───────┘               └──┘└───────────┘
typ    └┘                └┘  └───────┘              └──┘└───────────┘
doc                                                    └──┘             
txt                                                    └──┘             
par                                                    └──┘             
pid                                                      └┘             
st                                                    └────────────────┘└─
221      exact eq.symm (not_not.1 (mt h (list.not_mem_nil _))), by simp⟩
id             └─────┘  └─────┘    └┘   └──────────────┘
src      └────┘└─────┘ └─────┘└─┘ └┘  └──────────────┘└───┘     └──┘
typ      └────┘└─────┘ └─────┘└─┘ └┘ └──────────────┘└───┘     └──┘
doc      └────┘               └─┘                     └───┘     └──┘
txt      └────┘               └─┘                     └───┘     └──┘
par      └────┘               └─┘                     └───┘     └──┘
pid                          └─┘                     └───┘
st   ────────────────────────────────────────────────────────┘    └───┘
222  | (x :: l) := λ f h,
id       └┘         
src       └┘
typ      └┘         
223  if hfx : x = f x
id   └┘          
src  └┘         
typ  └┘          
224  then swap_factors_aux l f
id        └──────────────┘   
typ       └──────────────┘   
225    (λ y hy, list.mem_of_ne_of_mem (λ h : y = x, by simpa [h, hfx.symm] using hy) (h hy))
id         └┘  └───────────────────┘                                         └┘    └┘
src             └───────────────────┘                 └─────┘ └┘        └──────┘
typ        └┘  └───────────────────┘                └─────┘└┘└──────┘└──────┘└┘    └┘
doc                                                    └─────┘ └┘        └──────┘
txt                                                    └─────┘ └┘        └──────┘
par                                                    └─────┘ └┘        └──────┘
pid                                                          └┘        └────┘
st                                                    └───────────────────────────┘
226  else let m := swap_factors_aux l (swap x (f x) * f)
id        └─┘     └──────────────┘    └──┘         
src                                    └──┘         
typ       └─┘     └──────────────┘    └──┘         
doc                                    └──┘
227        (λ y hy, have f y ≠ y ∧ y ≠ x, from ne_and_ne_of_swap_mul_apply_ne_self hy,
id             └┘                      └─────────────────────────────────┘ └┘
src                                         └─────────────────────────────────┘
typ            └┘                      └─────────────────────────────────┘ └┘
228          list.mem_of_ne_of_mem this.2 (h this.1)) in
id           └───────────────────┘ └──┘    └──┘
src          └───────────────────┘              
typ          └───────────────────┘ └──┘    └──┘
229    ⟨swap x (f x) :: m.1,
id      └──┘        └┘ 
src     └──┘         └┘  
typ     └──┘        └┘ 
doc     └──┘
230    by rw [list.prod_cons, m.2.1, ← mul_assoc,
id            └────────────┘          └───────┘
src       └──┘└────────────┘└┘ └──────┘└───────┘└─
typ       └──┘└────────────┘└┘└──────┘└───────┘└─
doc       └──┘              └┘ └──────┘         └─
txt       └──┘              └┘ └──────┘         └─
par       └──┘              └┘ └──────┘         └─
pid         └┘              └┘ └──────┘         └─
st       └─────────────────┘└───┘└─────────────┘└─
231      mul_def (swap x (f x)), swap_swap, ← one_def, one_mul],
id       └─────┘  └──┘         └───────┘    └─────┘  └─────┘
src  ───┘└─────┘ └──┘    └──┘└───────┘└──┘└─────┘└┘└─────┘
typ  ───┘└─────┘ └──┘  └──┘└───────┘└──┘└─────┘└┘└─────┘
doc  ───┘        └──┘    └──┘         └──┘       └┘       
txt  ───┘                └──┘         └──┘       └┘       
par  ───┘                └──┘         └──┘       └┘       
pid  ───┘                └──┘         └──┘       └┘       
st   ─────────────────────────┘└─────────┘└─────────┘└───────┘
232    λ g hg, ((list.mem_cons_iff _ _ _).1 hg).elim (λ h, ⟨x, f x, hfx, h⟩) (m.2.2 _)⟩
id        └┘    └───────────────┘         └┘ └──┘               └─┘       
src              └───────────────┘            └──┘                             
typ       └┘    └───────────────┘         └┘ └──┘               └─┘       
233  
234  /-- `swap_factors` represents a permutation as a product of a list of transpositions.
235  The representation is non unique and depends on the linear order structure.
236  For types without linear order `trunc_swap_factors` can be used -/
237  def swap_factors [fintype α] [decidable_linear_order α] (f : perm α) :
id                     └─────┘    └────────────────────┘        └──┘ 
src                    └─────┘     └────────────────────┘         └──┘
typ                    └─────┘    └────────────────────┘        └──┘ 
doc                    └─────┘                                    └──┘
238    {l : list (perm α) // l.prod = f ∧ ∀ g ∈ l, is_swap g} :=
id         └──┘  └──┘      └───┘           └─────┘ 
src        └──┘  └──┘        └───┘              └─────┘
typ        └──┘  └──┘      └───┘           └─────┘ 
doc               └──┘        └───┘
239  swap_factors_aux ((@univ α _).sort (≤)) f (λ _ _, (mem_sort _).2 (mem_univ _))
id   └──────────────┘    └──┘    └──┘              └──────┘      └──────┘
src  └──────────────┘    └──┘     └──┘                 └──────┘      └──────┘
typ  └──────────────┘    └──┘    └──┘              └──────┘      └──────┘
doc                      └──┘     └──┘
240  
241  def trunc_swap_factors [fintype α] (f : perm α) :
id                           └─────┘        └──┘ 
src                          └─────┘         └──┘
typ                          └─────┘        └──┘ 
doc                          └─────┘         └──┘
242    trunc {l : list (perm α) // l.prod = f ∧ ∀ g ∈ l, is_swap g} :=
id     └───┘     └──┘  └──┘      └───┘           └─────┘ 
src    └───┘     └──┘  └──┘        └───┘              └─────┘
typ    └───┘     └──┘  └──┘      └───┘           └─────┘ 
doc    └───┘            └──┘        └───┘
243  quotient.rec_on_subsingleton (@univ α _).1
id   └──────────────────────────┘   └──┘    
src  └──────────────────────────┘   └──┘     
typ  └──────────────────────────┘   └──┘    
doc                                 └──┘
244  (λ l h, trunc.mk (swap_factors_aux l f h))
id         └──────┘  └──────────────┘   
src          └──────┘  └──────────────┘
typ        └──────┘  └──────────────┘   
doc          └──────┘
245  (show ∀ x, f x ≠ x → x ∈ (@univ α _).1, from λ _ _, mem_univ _)
id                       └──┘                 └──────┘
src                           └──┘                    └──────┘
typ                      └──┘                 └──────┘
doc                             └──┘
246  
247  @[elab_as_eliminator] lemma swap_induction_on [fintype α] {P : perm α → Prop} (f : perm α) :
id                                                  └─────┘        └──┘               └──┘ 
src                                                 └─────┘         └──┘                └──┘
typ                                                 └─────┘        └──┘               └──┘ 
doc    └────────────────┘                           └─────┘         └──┘                └──┘
248    P 1 → (∀ f x y, x ≠ y → P f → P (swap x y * f)) → P f :=
id                            └──┘          
src                                    └──┘     
typ                           └──┘          
doc                                     └──┘
249  begin
st   └─────
250    cases trunc.out (trunc_swap_factors f) with l hl,
id           └───────┘  └────────────────┘ 
src    └────┘└───────┘ └────────────────┘ └─────────┘
typ    └────┘└───────┘ └────────────────┘└─────────┘
doc    └────┘└───────┘                    └─────────┘
txt    └────┘                             └─────────┘
par    └────┘                             └─────────┘
pid                                      └────────┘
st   ─────────────────────────────────────────────────┘└─
251    induction l with g l ih generalizing f,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └─────────┘└─────────────┘
st   ───────────────────────────────────────┘└─
252    { simp [hl.1.symm] {contextual := tt} },
id             └┘                        └┘
src      └────┘  └───────┘ └────────────┘└┘└┘
typ      └────┘└┘└───────┘ └────────────┘└┘└┘
doc      └────┘  └───────┘ └────────────┘  └┘
txt      └────┘  └───────┘ └────────────┘  └┘
par      └────┘  └───────┘ └────────────┘  └┘
pid            └──────┘ └────────────┘  
st   ───┘└──────────────────────────────────┘└┘
253    { assume h1 hmul_swap,
src      └─────────────────┘
typ      └─────────────────┘
doc      └─────────────────┘
txt      └─────────────────┘
par      └─────────────────┘
pid      └─────────────────┘
st   ──────────────────────┘└─
254      rcases hl.2 g (by simp) with ⟨x, y, hxy⟩,
id              └┘   
src      └─────┘  └─┘    └──┘└────────────────┘
typ      └─────┘└┘└─┘   └──┘└────────────────┘
doc      └─────┘  └─┘    └──┘└────────────────┘
txt      └─────┘  └─┘    └──┘└────────────────┘
par      └─────┘  └─┘    └──┘└────────────────┘
pid              └─┘    └─────────────────────┘
st   ────────────────────┘└───┘└────────────────┘└─
255      rw [← hl.1, list.prod_cons, hxy.2],
id             └┘    └────────────┘  └─┘
src      └────┘  └──┘└────────────┘└┘   └─┘
typ      └────┘└┘└──┘└────────────┘└┘└─┘└─┘
doc      └────┘  └──┘              └┘   └─┘
txt      └────┘  └──┘              └┘   └─┘
par      └────┘  └──┘              └┘   └─┘
pid        └──┘  └──┘              └┘   └─┘
st   ───────────┘└────────────────┘└───┘└────
256      exact hmul_swap _ _ _ hxy.1 (ih _ ⟨rfl, λ v hv, hl.2 _ (list.mem_cons_of_mem _ hv)⟩ h1 hmul_swap) }
id                             └─┘    └┘    └─┘          └┘      └──────────────────┘        └┘ └───────┘
src      └────┘         └─────┘   └─┘   └─┘ └─┘└┘ └─────┘  └───┘ └──────────────────┘└─┘  └─┘           └┘
typ      └────┘         └─────┘└─┘└─┘ └┘└─┘ └─┘└┘ └─────┘└┘└───┘ └──────────────────┘└─┘  └─┘└┘└───────┘└┘
doc      └────┘         └─────┘   └─┘   └─┘    └┘ └─────┘  └───┘                     └─┘  └─┘           └┘
txt      └────┘         └─────┘   └─┘   └─┘    └┘ └─────┘  └───┘                     └─┘  └─┘           └┘
par      └────┘         └─────┘   └─┘   └─┘    └┘ └─────┘  └───┘                     └─┘  └─┘           └┘
pid                    └─────┘   └─┘   └─┘    └┘ └─────┘  └───┘                     └─┘  └─┘           
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
257  end
st   ──┘
258  
259  lemma swap_mul_swap_mul_swap {x y z : α} (hwz: x ≠ y) (hxz : x ≠ z) :
id                                                              
src                                                                
typ                                                             
260    swap y z * swap x y * swap y z = swap z x :=
id     └──┘    └──┘    └──┘    └──┘  
src    └──┘      └──┘      └──┘      └──┘
typ    └──┘    └──┘    └──┘    └──┘  
doc    └──┘       └──┘       └──┘       └──┘
261  equiv.ext _ _ $ λ n, by simp only [swap_apply_def, mul_apply]; split_ifs; cc
id   └───────┘                         └────────────┘  └───────┘
src  └───────┘               └─────────┘└────────────┘└┘└───────┘  └───────┘  └──
typ  └───────┘              └─────────┘└────────────┘└┘└───────┘  └───────┘  └──
doc                          └─────────┘              └┘           └───────┘  └──
txt                          └─────────┘              └┘           └───────┘  └──
par                          └─────────┘              └┘           └───────┘  └──
pid                              └──┘└┘              └┘                        
st                          └─────────────────────────────────────────────────────
262  
src  
typ  
doc  
txt  
par  
pid  
st   
263  lemma is_conj_swap {w x y z : α} (hwx : w ≠ x) (hyz : y ≠ z) : is_conj (swap w x) (swap y z) :=
id                                                           └─────┘  └──┘     └──┘  
src                                                               └─────┘  └──┘       └──┘
typ                                                          └─────┘  └──┘     └──┘  
doc                                                                          └──┘       └──┘
264  have h : ∀ {y z : α}, y ≠ z → w ≠ z →
id                               
src                                 
typ                              
265      (swap w y * swap x z) * swap w x * (swap w y * swap x z)⁻¹ = swap y z :=
id        └──┘    └──┘     └──┘     └──┘    └──┘   └┘  └──┘  
src       └──┘      └──┘       └──┘       └──┘      └──┘     └┘  └──┘
typ       └──┘    └──┘     └──┘     └──┘    └──┘   └┘  └──┘  
doc       └──┘       └──┘        └──┘        └──┘       └──┘          └──┘
266    λ y z hyz hwz, by rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y),
id         └─┘ └─┘         └─────────┘  └──────┘  └──────┘  └───────┘  └──┘  
src                      └──┘└─────────┘└┘└──────┘└┘└──────┘└┘└───────┘ └──┘  └──
typ        └─┘ └─┘     └──┘└─────────┘└┘└──────┘└┘└──────┘└┘└───────┘ └──┘└──
doc                      └──┘           └┘        └┘        └┘          └──┘  └──
txt                      └──┘           └┘        └┘        └┘                └──
par                      └──┘           └┘        └┘        └┘                └──
pid                        └┘           └┘        └┘        └┘                └──
st                      └──────────────┘└────────┘└────────┘└────────────────────┘└─
267      mul_assoc (swap w y),  ← mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz,
id       └───────┘  └──┘        └───────┘    └──┘     └────────────────────┘ └─┘ └─┘
src  ───┘└───────┘ └──┘  └────┘└───────┘└─┘ └──┘  └─┘└────────────────────┘      └─
typ  ───┘└───────┘ └──┘└────┘└───────┘└─┘ └──┘└─┘└────────────────────┘└─┘└─┘└─
doc  ───┘          └──┘  └────┘         └─┘ └──┘  └─┘                            └─
txt  ───┘                └────┘         └─┘       └─┘                            └─
par  ───┘                └────┘         └─┘       └─┘                            └─
pid  ───┘                └────┘         └─┘       └─┘                            └─
st   ───────────────────────┘└─────────────────────────┘└──────────────────────────────┘└─
268      ← mul_assoc, swap_mul_swap_mul_swap hwz.symm hyz.symm],
id         └───────┘  └────────────────────┘ └──────┘ └──────┘
src  ─────┘└───────┘└┘└────────────────────┘└──────┘└──────┘
typ  ─────┘└───────┘└┘└────────────────────┘└──────┘└──────┘
doc  ─────┘         └┘                                      
txt  ─────┘         └┘                                      
par  ─────┘         └┘                                      
pid  ─────┘         └┘                                      
st   ──────────────┘└────────────────────────────────────────┘
269  if hwz : w = z
id   └┘         
src  └┘         
typ  └┘         
270  then have hwy : w ≠ y, by cc,
id                     
src                           └┘
typ                         └┘
doc                            └┘
txt                            └┘
par                            └┘
st                            └─┘
271    ⟨swap w z * swap x y, by rw [swap_comm y z, h hyz.symm hwy]⟩
id      └──┘    └──┘           └───────┘     └──────┘ └─┘
src     └──┘      └──┘         └──┘└───────┘  └┘ └──────┘   
typ     └──┘    └──┘       └──┘└───────┘└┘└──────┘└─┘
doc     └──┘       └──┘         └──┘           └┘            
txt                             └──┘           └┘            
par                             └──┘           └┘            
pid                               └┘           └┘            
st                             └────────────────┘└──────────────┘
272  else ⟨swap w y * swap x z, h hyz hwz⟩
id        └──┘    └──┘     └─┘ └─┘
src        └──┘      └──┘
typ       └──┘    └──┘     └─┘ └─┘
doc        └──┘       └──┘
273  
274  /-- set of all pairs (⟨a, b⟩ : Σ a : fin n, fin n) such that b < a -/
275  def fin_pairs_lt (n : ℕ) : finset (Σ a : fin n, fin n) :=
id                             └────┘       └─┘  └─┘ 
src                            └────┘       └─┘   └─┘
typ                            └────┘       └─┘  └─┘ 
doc                             └────┘
276  (univ : finset (fin n)).sigma (λ a, (range a.1).attach_fin
id    └──┘   └────┘  └─┘   └───┘        └───┘   └────────┘
src   └──┘   └────┘  └─┘    └───┘         └───┘    └────────┘
typ   └──┘   └────┘  └─┘   └───┘        └───┘   └────────┘
doc   └──┘   └────┘         └───┘         └───┘
277    (λ m hm, lt_trans (mem_range.1 hm) a.2))
id         └┘  └──────┘  └───────┘  └┘  
src             └──────┘  └───────┘       
typ        └┘  └──────┘  └───────┘  └┘  
278  
279  lemma mem_fin_pairs_lt {n : ℕ} {a : Σ a : fin n, fin n} :
id                                           └─┘  └─┘ 
src                                          └─┘   └─┘
typ                                          └─┘  └─┘ 
280    a ∈ fin_pairs_lt n ↔ a.2 < a.1 :=
id       └──────────┘      
src       └──────────┘         
typ      └──────────┘      
doc        └──────────┘
281  by simp [fin_pairs_lt, fin.lt_def]
id            └──────────┘  └────────┘
src     └────┘└──────────┘└┘└────────┘└─
typ     └────┘└──────────┘└┘└────────┘└─
doc     └────┘└──────────┘└┘          └─
txt     └────┘            └┘          └─
par     └────┘            └┘          └─
pid                     └┘          
st     └────────────────────────────────
282  
src  
typ  
doc  
txt  
par  
pid  
st   
283  def sign_aux {n : ℕ} (a : perm (fin n)) : units ℤ :=
id                            └──┘  └─┘      └───┘ 
src                           └──┘  └─┘       └───┘ 
typ                           └──┘  └─┘      └───┘ 
doc                            └──┘
284  (fin_pairs_lt n).prod (λ x, if a x.1 ≤ a x.2 then -1 else 1)
id    └──────────┘  └──┘                      
src   └──────────┘   └──┘                           
typ   └──────────┘  └──┘                      
doc   └──────────┘   └──┘
285  
286  @[simp] lemma sign_aux_one (n : ℕ) : sign_aux (1 : perm (fin n)) = 1 :=
id                                       └──────┘      └──┘  └─┘    
src                                      └──────┘      └──┘  └─┘     
typ                                      └──────┘      └──┘  └─┘    
doc    └──┘                                             └──┘
287  begin
st   └─────
288    unfold sign_aux,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid          └───────┘
st   ────────────────┘└─
289    conv { to_rhs, rw ← @finset.prod_const_one _ (units ℤ)
id                          └───────────────────┘    └───┘
src    └─────┘└────┘└┘└───┘ └───────────────────┘└─┘ └───┘ └─
typ    └─────┘└────┘└┘└───┘ └───────────────────┘└─┘ └───┘ └─
txt    └─────┘└────┘└┘└───┘                      └─┘       └─
par    └─────┘└────┘└┘└───┘                      └─┘       └─
pid        └─────────────┘                      └─┘       └─
st   ───────┘└─────┘└─────────────────────────────────────────
290      (fin_pairs_lt n) },
id        └──────────┘ 
src  ───┘ └──────────┘ └┘
typ  ───┘ └──────────┘└┘
doc       └──────────┘
txt  ───┘              └┘
par  ───┘              └┘
pid  ───┘              └─┘
st   ────────────────────┘└┘
291    exact finset.prod_congr rfl (λ a ha, if_neg
id           └───────────────┘ └─┘          └────┘
src    └────┘└───────────────┘└─┘  └─────┘└────┘
typ    └────┘└───────────────┘└─┘  └─────┘└────┘
doc    └────┘                      └─────┘      
txt    └────┘                      └─────┘      
par    └────┘                      └─────┘      
pid                               └─────┘      
st   ──────────────────────────────────────────────
292      (not_le_of_gt (mem_fin_pairs_lt.1 ha)))
id        └──────────┘  └──────────────┘
src  ───┘ └──────────┘ └──────────────┘└─┘  └──┘
typ  ───┘ └──────────┘ └──────────────┘└─┘  └──┘
doc  ───┘                              └─┘  └──┘
txt  ───┘                              └─┘  └──┘
par  ───┘                              └─┘  └──┘
pid  ───┘                              └─┘  └─┘
st   ───────────────────────────────────────────┘
293  end
st   └─┘
294  
295  def sign_bij_aux {n : ℕ} (f : perm (fin n)) (a : Σ a : fin n, fin n) :
id                                └──┘  └─┘              └─┘  └─┘ 
src                               └──┘  └─┘               └─┘   └─┘
typ                               └──┘  └─┘              └─┘  └─┘ 
doc                                └──┘
296    Σ a : fin n, fin n :=
id          └─┘  └─┘ 
src         └─┘   └─┘
typ         └─┘  └─┘ 
297  if hxa : f a.2 < f a.1 then ⟨f a.1, f a.2⟩ else ⟨f a.2, f a.1⟩
id   └┘                                      
src  └┘                                                   
typ  └┘                                      
298  
299  lemma sign_bij_aux_inj {n : ℕ} {f : perm (fin n)} : ∀ a b : Σ a : fin n, fin n,
id                                      └──┘  └─┘                   └─┘  └─┘ 
src                                     └──┘  └─┘                    └─┘   └─┘
typ                                     └──┘  └─┘                   └─┘  └─┘ 
doc                                      └──┘
300     a ∈ fin_pairs_lt n → b ∈ fin_pairs_lt n →
id        └──────────┘      └──────────┘ 
src        └──────────┘        └──────────┘
typ       └──────────┘      └──────────┘ 
doc         └──────────┘         └──────────┘
301     sign_bij_aux f a = sign_bij_aux f b → a = b :=
id      └──────────┘    └──────────┘       
src     └──────────┘      └──────────┘         
typ     └──────────┘    └──────────┘       
302  λ ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ha hb h, begin
id                     └┘ └┘ 
typ                    └┘ └┘ 
st                                └─────
303    unfold sign_bij_aux at h,
src    └──────────────────────┘
typ    └──────────────────────┘
doc    └──────────────────────┘
txt    └──────────────────────┘
par    └──────────────────────┘
pid          └───────────┘└───┘
st   ─────────────────────────┘└─
304    rw mem_fin_pairs_lt at *,
id        └──────────────┘
src    └─┘└──────────────┘└───┘
typ    └─┘└──────────────┘└───┘
doc    └─┘                └───┘
txt    └─┘                └───┘
par    └─┘                └───┘
pid                      └───┘
st   ─────────────────────────┘└─
305    have : ¬b₁ < b₂ := not_lt_of_ge (le_of_lt hb),
id             └┘  └┘    └──────────┘  └──────┘ └┘
src    └─────┘     └──┘└──────────┘ └──────┘  
typ    └─────┘ └┘└┘└──┘└──────────┘ └──────┘└┘
doc    └─────┘      └──┘                       
txt    └─────┘      └──┘                       
par    └─────┘      └──┘                       
pid    └───┘└┘      └──┘                       
st   ──────────────────────────────────────────────┘└─
306    split_ifs at h;
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid             └───┘
st   ──────────────────
307    simp [*, injective.eq_iff f.injective, sigma.mk.inj_eq] at *
id              └──────────────┘ └─────────┘  └─────────────┘
src    └───────┘└──────────────┘└─────────┘└┘└─────────────┘└─────┘
typ    └───────┘└──────────────┘└─────────┘└┘└─────────────┘└─────┘
doc    └───────┘                           └┘               └─────┘
txt    └───────┘                           └┘               └─────┘
par    └───────┘                           └┘               └─────┘
pid        └──┘                           └┘               └──┘
st   ──────────────────────────────────────────────────────────────┘
308  end
st   └─┘
309  
310  lemma sign_bij_aux_surj {n : ℕ} {f : perm (fin n)} : ∀ a ∈ fin_pairs_lt n,
id                                       └──┘  └─┘           └──────────┘ 
src                                      └──┘  └─┘             └──────────┘
typ                                      └──┘  └─┘           └──────────┘ 
doc                                       └──┘                  └──────────┘
311    ∃ b ∈ fin_pairs_lt n, a = sign_bij_aux f b :=
id         └──────────┘    └──────────┘  
src         └──────────┘      └──────────┘
typ        └──────────┘    └──────────┘  
doc          └──────────┘
312  λ ⟨a₁, a₂⟩ ha,
id     └┘  └┘  └┘
typ    └┘  └┘  └┘
313  if hxa : f⁻¹ a₂ < f⁻¹ a₁
id   └┘       └┘     └┘
src  └┘        └┘      └┘
typ  └┘       └┘     └┘
314  then ⟨⟨f⁻¹ a₁, f⁻¹ a₂⟩, mem_fin_pairs_lt.2 hxa,
id          └┘     └┘      └──────────────┘  └─┘
src          └┘      └┘      └──────────────┘
typ         └┘     └┘      └──────────────┘  └─┘
315    by dsimp [sign_bij_aux];
id               └──────────┘
src       └─────┘└──────────┘
typ       └─────┘└──────────┘
doc       └─────┘            
txt       └─────┘            
par       └─────┘            
pid                        
st       └──────────────────────
316      rw [apply_inv_self, apply_inv_self, dif_pos (mem_fin_pairs_lt.1 ha)]⟩
id           └────────────┘  └────────────┘  └─────┘  └──────────────┘   └┘
src      └──┘└────────────┘└┘└────────────┘└┘└─────┘ └──────────────┘└─┘  └┘
typ      └──┘└────────────┘└┘└────────────┘└┘└─────┘ └──────────────┘└─┘└┘└┘
doc      └──┘              └┘              └┘                        └─┘  └┘
txt      └──┘              └┘              └┘                        └─┘  └┘
par      └──┘              └┘              └┘                        └─┘  └┘
pid        └┘              └┘              └┘                        └─┘  └┘
st   ───────┘└────────────┘└──────────────┘└───────────────────────────────┘
317  else ⟨⟨f⁻¹ a₂, f⁻¹ a₁⟩, mem_fin_pairs_lt.2 $ lt_of_le_of_ne
id         └┘     └┘      └──────────────┘    └────────────┘
src          └┘      └┘      └──────────────┘    └────────────┘
typ        └┘     └┘      └──────────────┘    └────────────┘
318    (le_of_not_gt hxa) $ λ h,
id      └──────────┘ └─┘      
src     └──────────┘
typ     └──────────┘ └─┘      
319      by simpa [mem_fin_pairs_lt, (f⁻¹).injective h, lt_irrefl] using ha,
id                 └──────────────┘   └┘              └───────┘        └┘
src         └─────┘└──────────────┘└┘  └┘└──────────┘ └┘└───────┘└──────┘
typ         └─────┘└──────────────┘└┘ └┘└──────────┘└┘└───────┘└──────┘└┘
doc         └─────┘                └┘    └──────────┘ └┘         └──────┘
txt         └─────┘                └┘    └──────────┘ └┘         └──────┘
par         └─────┘                └┘    └──────────┘ └┘         └──────┘
pid                              └┘    └──────────┘ └┘         └────┘
st         └──────────────────────────────────────────────────────────────┘
320    by dsimp [sign_bij_aux];
id               └──────────┘
src       └─────┘└──────────┘
typ       └─────┘└──────────┘
doc       └─────┘            
txt       └─────┘            
par       └─────┘            
pid                        
st       └──────────────────────
321      rw [apply_inv_self, apply_inv_self,
id           └────────────┘  └────────────┘
src      └──┘└────────────┘└┘└────────────┘└─
typ      └──┘└────────────┘└┘└────────────┘└─
doc      └──┘              └┘              └─
txt      └──┘              └┘              └─
par      └──┘              └┘              └─
pid        └┘              └┘              └─
st   ───────┘└────────────┘└──────────────┘└─
322        dif_neg (not_lt_of_ge (le_of_lt (mem_fin_pairs_lt.1 ha)))]⟩
id         └─────┘  └──────────┘  └──────┘  └──────────────┘   └┘
src  ─────┘└─────┘ └──────────┘ └──────┘ └──────────────┘└─┘  └──┘
typ  ─────┘└─────┘ └──────────┘ └──────┘ └──────────────┘└─┘└┘└──┘
doc  ─────┘                                              └─┘  └──┘
txt  ─────┘                                              └─┘  └──┘
par  ─────┘                                              └─┘  └──┘
pid  ─────┘                                              └─┘  └──┘
st   ──────────────────────────────────────────────────────────────┘
323  
324  lemma sign_bij_aux_mem {n : ℕ} {f : perm (fin n)}: ∀ a : Σ a : fin n, fin n,
id                                      └──┘  └─┘                └─┘  └─┘ 
src                                     └──┘  └─┘                 └─┘   └─┘
typ                                     └──┘  └─┘                └─┘  └─┘ 
doc                                      └──┘
325    a ∈ fin_pairs_lt n → sign_bij_aux f a ∈ fin_pairs_lt n :=
id       └──────────┘    └──────────┘    └──────────┘ 
src       └──────────┘     └──────────┘      └──────────┘
typ      └──────────┘    └──────────┘    └──────────┘ 
doc        └──────────┘                        └──────────┘
326  λ ⟨a₁, a₂⟩ ha, begin
id             └┘
typ            └┘
st                  └─────
327    unfold sign_bij_aux,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid          └───────────┘
st   ────────────────────┘└─
328    split_ifs with h,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid             └────┘
st   ─────────────────┘└─
329    { exact mem_fin_pairs_lt.2 h },
id             └──────────────┘   
src      └────┘└──────────────┘└─┘ 
typ      └────┘└──────────────┘└─┘
doc      └────┘                └─┘ 
txt      └────┘                └─┘ 
par      └────┘                └─┘ 
pid                           └─┘ 
st   ───┘└─────────────────────────┘└┘
330    { exact mem_fin_pairs_lt.2
src      └────┘                └──
typ      └────┘                └──
doc      └────┘                └──
txt      └────┘                └──
par      └────┘                └──
pid                           └──
st   ─────────────────────────────
331      (lt_of_le_of_ne (le_of_not_gt h)
id        └────────────┘  └──────────┘ 
src  ───┘ └────────────┘ └──────────┘ └─
typ  ───┘ └────────────┘ └──────────┘└─
doc  ───┘                             └─
txt  ───┘                             └─
par  ───┘                             └─
pid  ───┘                             └─
st   ─────────────────────────────────────
332        (λ h, ne_of_lt (mem_fin_pairs_lt.1 ha) (f.injective h.symm))) }
id               └──────┘  └──────────────┘   └┘   └─────────┘  └───┘
src  ─────┘  └──┘└──────┘ └──────────────┘└─┘  └┘ └─────────┘ └───┘└──┘
typ  ─────┘  └──┘└──────┘ └──────────────┘└─┘└┘└┘ └─────────┘ └───┘└──┘
doc  ─────┘  └──┘                         └─┘  └┘                  └──┘
txt  ─────┘  └──┘                         └─┘  └┘                  └──┘
par  ─────┘  └──┘                         └─┘  └┘                  └──┘
pid  ─────┘  └──┘                         └─┘  └┘                  └─┘
st   ───────────────────────────────────────────────────────────────────┘└─
333  end
st   ──┘
334  
335  @[simp] lemma sign_aux_inv {n : ℕ} (f : perm (fin n)) : sign_aux f⁻¹ = sign_aux f :=
id                                          └──┘  └─┘      └──────┘ └┘  └──────┘ 
src                                         └──┘  └─┘       └──────┘  └┘  └──────┘
typ                                         └──┘  └─┘      └──────┘ └┘  └──────┘ 
doc    └──┘                                  └──┘
336  prod_bij (λ a ha, sign_bij_aux f⁻¹ a)
id   └──────┘     └┘  └──────────┘ └┘ 
src  └──────┘          └──────────┘  └┘
typ  └──────┘     └┘  └──────────┘ └┘ 
337  sign_bij_aux_mem
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
338  (λ ⟨a, b⟩ hab, if h : f⁻¹ b < f⁻¹ a
id          └─┘  └┘     └┘    └┘
src                 └┘      └┘     └┘
typ         └─┘  └┘     └┘    └┘
339    then by rw [sign_bij_aux, dif_pos h, if_neg (not_le_of_gt h), apply_inv_self,
id                 └──────────┘  └─────┘   └────┘  └──────────┘    └────────────┘
src            └──┘└──────────┘└┘└─────┘ └┘└────┘ └──────────┘ └─┘└────────────┘└─
typ            └──┘└──────────┘└┘└─────┘└┘└────┘ └──────────┘└─┘└────────────┘└─
doc            └──┘            └┘        └┘                    └─┘              └─
txt            └──┘            └┘        └┘                    └─┘              └─
par            └──┘            └┘        └┘                    └─┘              └─
pid              └┘            └┘        └┘                    └─┘              └─
st            └───────────────┘└─────────┘└───────────────────────┘└──────────────┘└─
340      apply_inv_self, if_neg (not_le_of_gt $ mem_fin_pairs_lt.1 hab)]
id       └────────────┘  └────┘  └──────────┘   └──────────────┘   └─┘
src  ───┘└────────────┘└┘└────┘ └──────────┘ └──────────────┘└─┘   └──
typ  ───┘└────────────┘└┘└────┘ └──────────┘ └──────────────┘└─┘└─┘└──
doc  ───┘              └┘                                    └─┘   └──
txt  ───┘              └┘                                    └─┘   └──
par  ───┘              └┘                                    └─┘   └──
pid  ───┘              └┘                                    └─┘   └┘
st   ─────────────────┘└──────────────────────────────────────────────┘
341    else by rw [sign_bij_aux, if_pos (le_of_not_gt h), dif_neg h, apply_inv_self,
id                 └──────────┘  └────┘  └──────────┘    └─────┘   └────────────┘
src  ─┘        └──┘└──────────┘└┘└────┘ └──────────┘ └─┘└─────┘ └┘└────────────┘└─
typ  ─┘        └──┘└──────────┘└┘└────┘ └──────────┘└─┘└─────┘└┘└────────────┘└─
doc  ─┘        └──┘            └┘                    └─┘        └┘              └─
txt  ─┘        └──┘            └┘                    └─┘        └┘              └─
par  ─┘        └──┘            └┘                    └─┘        └┘              └─
pid  ─┘          └┘            └┘                    └─┘        └┘              └─
st   ─┘       └───────────────┘└───────────────────────┘└─────────┘└──────────────┘└─
342      apply_inv_self, if_pos (le_of_lt $ mem_fin_pairs_lt.1 hab)])
id       └────────────┘  └────┘  └──────┘   └──────────────┘   └─┘
src  ───┘└────────────┘└┘└────┘ └──────┘ └──────────────┘└─┘   └┘
typ  ───┘└────────────┘└┘└────┘ └──────┘ └──────────────┘└─┘└─┘└┘
doc  ───┘              └┘                                └─┘   └┘
txt  ───┘              └┘                                └─┘   └┘
par  ───┘              └┘                                └─┘   └┘
pid  ───┘              └┘                                └─┘   └┘
st   ─────────────────┘└──────────────────────────────────────────┘
343  sign_bij_aux_inj
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
344  sign_bij_aux_surj
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
345  
346  lemma sign_aux_mul {n : ℕ} (f g : perm (fin n)) :
id                                    └──┘  └─┘ 
src                                   └──┘  └─┘
typ                                   └──┘  └─┘ 
doc                                    └──┘
347    sign_aux (f * g) = sign_aux f * sign_aux g :=
id     └──────┘       └──────┘   └──────┘ 
src    └──────┘         └──────┘    └──────┘
typ    └──────┘       └──────┘   └──────┘ 
348  begin
st   └─────
349    rw ← sign_aux_inv g,
id          └──────────┘ 
src    └───┘└──────────┘
typ    └───┘└──────────┘
doc    └───┘            
txt    └───┘            
par    └───┘            
pid      └─┘            
st   ────────────────────┘└─
350    unfold sign_aux,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid          └───────┘
st   ────────────────┘└─
351    rw  ← prod_mul_distrib,
id           └──────────────┘
src    └────┘└──────────────┘
typ    └────┘└──────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid      └──┘
st   ───────────────────────┘└─
352    refine prod_bij (λ a ha, sign_bij_aux g a) sign_bij_aux_mem _
id            └──────┘          └──────────┘     └──────────────┘
src    └─────┘└──────┘  └─────┘└──────────┘  └┘└──────────────┘└──
typ    └─────┘└──────┘  └─────┘└──────────┘ └┘└──────────────┘└──
doc    └─────┘          └─────┘              └┘                └──
txt    └─────┘          └─────┘              └┘                └──
par    └─────┘          └─────┘              └┘                └──
pid                    └─────┘              └┘                └──
st   ────────────────────────────────────────────────────────────────
353      sign_bij_aux_inj sign_bij_aux_surj,
id       └──────────────┘ └───────────────┘
src  ───┘└──────────────┘└───────────────┘
typ  ───┘└──────────────┘└───────────────┘
doc  ───┘                
txt  ───┘                
par  ───┘                
pid  ───┘                
st   ─────────────────────────────────────┘└─
354    rintros ⟨a, b⟩ hab,
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid           └─────────┘
st   ───────────────────┘└─
355    rw [sign_bij_aux, mul_apply, mul_apply],
id         └──────────┘  └───────┘  └───────┘
src    └──┘└──────────┘└┘└───────┘└┘└───────┘
typ    └──┘└──────────┘└┘└───────┘└┘└───────┘
doc    └──┘            └┘         └┘         
txt    └──┘            └┘         └┘         
par    └──┘            └┘         └┘         
pid      └┘            └┘         └┘         
st   ─────────────────┘└─────────┘└─────────┘└──
356    rw mem_fin_pairs_lt at hab,
id        └──────────────┘
src    └─┘└──────────────┘└─────┘
typ    └─┘└──────────────┘└─────┘
doc    └─┘                └─────┘
txt    └─┘                └─────┘
par    └─┘                └─────┘
pid                      └─────┘
st   ───────────────────────────┘└─
357    by_cases h : g b < g a,
id                       
src    └───────┘ └─┘   
typ    └───────┘ └─┘ 
doc    └───────┘ └─┘    
txt    └───────┘ └─┘    
par    └───────┘ └─┘    
pid             └─┘    
st   ───────────────────────┘└─
358    { rw dif_pos h,
id          └─────┘ 
src      └─┘└─────┘
typ      └─┘└─────┘
doc      └─┘       
txt      └─┘       
par      └─┘       
pid               
st   ───┘└──────────┘└─
359      simp [not_le_of_gt hab]; congr },
id             └──────────┘ └─┘
src      └────┘└──────────┘     └────┘
typ      └────┘└──────────┘└─┘  └────┘
doc      └────┘               
txt      └────┘                 └────┘
par      └────┘                 └────┘
pid                                
st   ──────────────────────────────────┘└┘
360    { rw [dif_neg h, inv_apply_self, inv_apply_self, if_pos (le_of_lt hab)],
id           └─────┘   └────────────┘  └────────────┘  └────┘  └──────┘ └─┘
src      └──┘└─────┘ └┘└────────────┘└┘└────────────┘└┘└────┘ └──────┘   └┘
typ      └──┘└─────┘└┘└────────────┘└┘└────────────┘└┘└────┘ └──────┘└─┘└┘
doc      └──┘        └┘              └┘              └┘                  └┘
txt      └──┘        └┘              └┘              └┘                  └┘
par      └──┘        └┘              └┘              └┘                  └┘
pid        └┘        └┘              └┘              └┘                  └┘
st   ────────────────┘└──────────────┘└──────────────┘└─────────────────────┘└──
361      by_cases h₁ : f (g b) ≤ f (g a),
id                                
src      └───────┘  └─┘    └┘    
typ      └───────┘  └─┘   └┘ 
doc      └───────┘  └─┘    └┘     
txt      └───────┘  └─┘    └┘     
par      └───────┘  └─┘    └┘     
pid                └─┘    └┘     
st   ──────────────────────────────────┘└─
362      { have : f (g b) ≠ f (g a),
id                           
src        └─────┘    └┘    
typ        └─────┘   └┘ 
doc        └─────┘    └┘     
txt        └─────┘    └┘     
par        └─────┘    └┘     
pid        └───┘└┘    └┘     
st   ─────┘└──────────────────────┘└─
363        { rw [ne.def, injective.eq_iff f.injective,
id               └────┘  └──────────────┘ └─────────┘
src          └──┘└────┘└┘└──────────────┘└─────────┘└─
typ          └──┘└────┘└┘└──────────────┘└─────────┘└─
doc          └──┘      └┘                           └─
txt          └──┘      └┘                           └─
par          └──┘      └┘                           └─
pid            └┘      └┘                           └─
st   ───────┘└────────┘└────────────────────────────┘└─
364            injective.eq_iff g.injective];
id             └──────────────┘ └─────────┘
src  ─────────┘└──────────────┘└─────────┘
typ  ─────────┘└──────────────┘└─────────┘
doc  ─────────┘                           
txt  ─────────┘                           
par  ─────────┘                           
pid  ─────────┘                           
st   ─────────────────────────────────────┘└─
365          exact ne_of_lt hab },
id                 └──────┘ └─┘
src          └────┘└──────┘   
typ          └────┘└──────┘└─┘
doc          └────┘           
txt          └────┘           
par          └────┘           
pid                          
st   ──────────────────────────┘└┘
366        rw [if_pos h₁, if_neg (not_le_of_gt  (lt_of_le_of_ne h₁ this))],
id             └────┘ └┘  └────┘  └──────────┘   └────────────┘ └┘ └──┘
src        └──┘└────┘  └┘└────┘ └──────────┘└┘ └────────────┘      └─┘
typ        └──┘└────┘└┘└┘└────┘ └──────────┘└┘ └────────────┘└┘└──┘└─┘
doc        └──┘        └┘                   └┘                     └─┘
txt        └──┘        └┘                   └┘                     └─┘
par        └──┘        └┘                   └┘                     └─┘
pid          └┘        └┘                   └┘                     └─┘
st   ──────────────────┘└───────────────────────────────────────────────┘└──
367        refl },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└┘
368      { rw [if_neg h₁, if_pos (le_of_lt (lt_of_not_ge h₁))],
id             └────┘ └┘  └────┘  └──────┘  └──────────┘ └┘
src        └──┘└────┘  └┘└────┘ └──────┘ └──────────┘  └─┘
typ        └──┘└────┘└┘└┘└────┘ └──────┘ └──────────┘└┘└─┘
doc        └──┘        └┘                              └─┘
txt        └──┘        └┘                              └─┘
par        └──┘        └┘                              └─┘
pid          └┘        └┘                              └─┘
st   ──────────────────┘└───────────────────────────────────┘└──
369        refl } }
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└───
370  end
st   ──┘
371  
372  instance sign_aux.is_group_hom {n : ℕ} : is_group_hom (@sign_aux n) := { map_mul := sign_aux_mul }
id                                           └──────────┘   └──────┘                   └──────────┘
src                                          └──────────┘   └──────┘                    └──────────┘
typ                                          └──────────┘   └──────┘                   └──────────┘
doc                                           └──────────┘
373  
374  private lemma sign_aux_swap_zero_one {n : ℕ} (hn : 2 ≤ n) :
id                                                        
src                                                      
typ                                                       
375    sign_aux (swap (⟨0, lt_of_lt_of_le dec_trivial hn⟩ : fin n)
id     └──────┘  └──┘      └────────────┘ └─────────┘ └┘    └─┘ 
src    └──────┘  └──┘      └────────────┘ └─────────┘       └─┘
typ    └──────┘  └──┘      └────────────┘ └─────────┘ └┘    └─┘ 
doc              └──┘                     └─────────┘
376    ⟨1, lt_of_lt_of_le dec_trivial hn⟩) = -1 :=
id         └────────────┘ └─────────┘ └┘    
src        └────────────┘ └─────────┘       
typ        └────────────┘ └─────────┘ └┘    
doc                       └─────────┘
377  let zero : fin n := ⟨0, lt_of_lt_of_le dec_trivial hn⟩ in
id              └─┘         └────────────┘ └─────────┘ └┘
src             └─┘          └────────────┘ └─────────┘
typ             └─┘         └────────────┘ └─────────┘ └┘
doc                                         └─────────┘
378  let one : fin n := ⟨1, lt_of_lt_of_le dec_trivial hn⟩ in
id             └─┘         └────────────┘ └─────────┘ └┘
src            └─┘          └────────────┘ └─────────┘
typ            └─┘         └────────────┘ └─────────┘ └┘
doc                                        └─────────┘
379  have hzo : zero < one := dec_trivial,
id              └──┘  └─┘    └─────────┘
src                          └─────────┘
typ             └──┘  └─┘    └─────────┘
doc                           └─────────┘
380  show _ = (finset.singleton (⟨one, zero⟩ : Σ a : fin n, fin n)).prod
id            └──────────────┘   └─┘  └──┘         └─┘  └─┘   └──┘
src           └──────────────┘                     └─┘   └─┘    └──┘
typ           └──────────────┘   └─┘  └──┘         └─┘  └─┘   └──┘
doc            └──────────────┘                                    └──┘
381    (λ x : Σ a : fin n, fin n, if (equiv.swap zero one) x.1
id                 └─┘  └─┘       └────────┘ └──┘ └─┘  
src                └─┘   └─┘        └────────┘            
typ                └─┘  └─┘       └────────┘ └──┘ └─┘  
doc                                   └────────┘
382    ≤ swap zero one x.2 then (-1 : units ℤ) else 1),
id      └──┘ └──┘ └─┘             └───┘ 
src     └──┘                       └───┘ 
typ     └──┘ └──┘ └─┘             └───┘ 
doc      └──┘
383  begin
st   └─────
384    refine eq.symm (prod_subset (λ ⟨x₁, x₂⟩, by simp [mem_fin_pairs_lt, hzo] {contextual := tt})
id            └─────┘  └─────────┘                       └──────────────┘  └─┘                 └┘
src    └─────┘└─────┘ └─────────┘  └┘  └┘  └─┘  └────┘└──────────────┘└┘   └┘ └────────────┘└┘└─
typ    └─────┘└─────┘ └─────────┘  └┘  └┘  └─┘  └────┘└──────────────┘└┘└─┘└┘ └────────────┘└┘└─
doc    └─────┘                     └┘  └┘  └─┘  └────┘                └┘   └┘ └────────────┘  └─
txt    └─────┘                     └┘  └┘  └─┘  └────┘                └┘   └┘ └────────────┘  └─
par    └─────┘                     └┘  └┘  └─┘  └────┘                └┘   └┘ └────────────┘  └─
pid                               └┘  └┘  └─┘  └─────┘                └┘   └┘ └────────────┘  └──
st   ────────────────────────────────────────────┘└──────────────────────────────────────────────┘└─
385      (λ a ha₁ ha₂, _)),
src  ───┘  └─────────────┘
typ  ───┘  └─────────────┘
doc  ───┘  └─────────────┘
txt  ───┘  └─────────────┘
par  ───┘  └─────────────┘
pid  ───┘  └─────────────┘
st   ────────────────────┘└─
386    rcases a with ⟨⟨a₁, ha₁⟩, ⟨a₂, ha₂⟩⟩,
id            
src    └─────┘ └──────────────────────────┘
typ    └─────┘└──────────────────────────┘
doc    └─────┘ └──────────────────────────┘
txt    └─────┘ └──────────────────────────┘
par    └─────┘ └──────────────────────────┘
pid           └──────────────────────────┘
st   ─────────────────────────────────────┘└─
387    replace ha₁ : a₂ < a₁ := mem_fin_pairs_lt.1 ha₁,
id                   └┘  └┘    └──────────────┘   └─┘
src    └────────────┘    └──┘└──────────────┘└─┘
typ    └────────────┘└┘└┘└──┘└──────────────┘└─┘└─┘
doc    └────────────┘     └──┘                └─┘
txt    └────────────┘     └──┘                └─┘
par    └────────────┘     └──┘                └─┘
pid           └──┘└─┘     └──┘                └─┘
st   ────────────────────────────────────────────────┘└─
388    simp only [swap_apply_def],
id                └────────────┘
src    └─────────┘└────────────┘
typ    └─────────┘└────────────┘
doc    └─────────┘              
txt    └─────────┘              
par    └─────────┘              
pid        └──┘└┘              
st   ───────────────────────────┘└─
389    have : ¬ 1 ≤ a₂ → a₂ = 0, from λ h, nat.le_zero_iff.1 (nat.le_of_lt_succ (lt_of_not_ge h)),
id                     └┘               └─────────────┘    └───────────────┘  └──────────┘
src    └─────┘ └─┘     └┘  └───┘ └──┘└─────────────┘└─┘ └───────────────┘ └──────────┘ └┘
typ    └─────┘└─┘   └┘└┘  └───┘ └──┘└─────────────┘└─┘ └───────────────┘ └──────────┘ └┘
doc    └─────┘ └─┘       └┘  └───┘ └──┘               └─┘                                └┘
txt    └─────┘ └─┘       └┘  └───┘ └──┘               └─┘                                └┘
par    └─────┘ └─┘       └┘  └───┘ └──┘               └─┘                                └┘
pid    └───┘└┘ └─┘         └───┘ └──┘               └─┘                                └┘
st   ─────────────────────────┘└────────────────────────────────────────────────────────────────┘└─
390    have : a₁ ≤ 1 → a₁ = 0 ∨ a₁ = 1, from nat.cases_on a₁ (λ _, or.inl rfl)
id                            └┘                        └┘       └────┘
src    └─────┘   └─┘    └─┘   └┘  └───┘                └──┘└────┘   └─
typ    └─────┘  └─┘    └─┘└┘ └┘  └───┘            └┘  └──┘└────┘   └─
doc    └─────┘   └─┘    └─┘    └┘  └───┘                └──┘         └─
txt    └─────┘   └─┘    └─┘    └┘  └───┘                └──┘         └─
par    └─────┘   └─┘    └─┘    └┘  └───┘                └──┘         └─
pid    └───┘└┘   └─┘    └─┘      └───┘                └──┘         └─
st   ────────────────────────────────┘└────────────────────────────────────────
391      (λ a₁, nat.cases_on a₁ (λ _, or.inr rfl) (λ _ h, absurd h dec_trivial)),
id              └──────────┘          └────┘ └─┘          └────┘
src  ───┘  └───┘└──────────┘    └──┘└────┘└─┘└┘  └────┘└────┘            └┘
typ  ───┘  └───┘└──────────┘    └──┘└────┘└─┘└┘  └────┘└────┘            └┘
doc  ───┘  └───┘                └──┘         └┘  └────┘                  └┘
txt  ───┘  └───┘                └──┘         └┘  └────┘                  └┘
par  ───┘  └───┘                └──┘         └┘  └────┘                  └┘
pid  ───┘  └───┘                └──┘         └┘  └────┘                  └┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
392    split_ifs;
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ─────────────
393    simp [*, lt_irrefl, -not_lt, not_le.symm, -not_le, le_refl, fin.lt_def, fin.le_def, nat.zero_le,
id              └───────┘                                 └─────┘  └────────┘  └────────┘  └─────────┘
src    └───────┘└───────┘└─────────┘           └─────────┘└─────┘└┘└────────┘└┘└────────┘└┘└─────────┘└─
typ    └───────┘└───────┘└─────────┘└─────────┘└─────────┘└─────┘└┘└────────┘└┘└────────┘└┘└─────────┘└─
doc    └───────┘         └─────────┘           └─────────┘       └┘          └┘          └┘           └─
txt    └───────┘         └─────────┘           └─────────┘       └┘          └┘          └┘           └─
par    └───────┘         └─────────┘           └─────────┘       └┘          └┘          └┘           └─
pid        └──┘         └─────────┘           └─────────┘       └┘          └┘          └┘           └─
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
394      zero, one, iff.intro fin.veq_of_eq fin.eq_of_veq, nat.le_zero_iff] at *,
id       └──┘  └─┘  └───────┘ └───────────┘ └───────────┘  └─────────────┘
src  ───┘    └┘   └┘└───────┘└───────────┘└───────────┘└┘└─────────────┘└────┘
typ  ───┘└──┘└┘└─┘└┘└───────┘└───────────┘└───────────┘└┘└─────────────┘└────┘
doc  ───┘    └┘   └┘                                   └┘               └────┘
txt  ───┘    └┘   └┘                                   └┘               └────┘
par  ───┘    └┘   └┘                                   └┘               └────┘
pid  ───┘    └┘   └┘                                   └┘               └──┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
395  end
st   ──┘
396  
397  lemma sign_aux_swap : ∀ {n : ℕ} {x y : fin n} (hxy : x ≠ y),
id                                        └─┘            
src                                        └─┘             
typ                                       └─┘            
398    sign_aux (swap x y) = -1
id     └──────┘  └──┘     
src    └──────┘  └──┘       
typ    └──────┘  └──┘     
doc              └──┘
399  | 0 := dec_trivial
id          └─────────┘
src         └─────────┘
typ         └─────────┘
doc         └─────────┘
400  | 1 := dec_trivial
id          └─────────┘
src         └─────────┘
typ         └─────────┘
doc         └─────────┘
401  | (n+2) := λ x y hxy,
id                └─┘
src      
typ               └─┘
402  have h2n : 2 ≤ n + 2 := dec_trivial,
id                         └─────────┘
src                        └─────────┘
typ                        └─────────┘
doc                          └─────────┘
403  by rw [← is_conj_iff_eq, ← sign_aux_swap_zero_one h2n];
id            └────────────┘    └────────────────────┘ └─┘
src     └────┘└────────────┘└──┘└────────────────────┘   
typ     └────┘└────────────┘└──┘└────────────────────┘└─┘
doc     └────┘              └──┘                         
txt     └────┘              └──┘                         
par     └────┘              └──┘                         
pid       └──┘              └──┘                         
st     └───────────────────┘└────────────────────────────┘└─
404    exact is_group_hom.is_conj _ (is_conj_swap hxy dec_trivial)
id           └──────────────────┘    └──────────┘ └─┘ └─────────┘
src    └────┘└──────────────────┘└─┘ └──────────┘   └─────────┘└─
typ    └────┘└──────────────────┘└─┘ └──────────┘└─┘└─────────┘└─
doc    └────┘                    └─┘                           └─
txt    └────┘                    └─┘                           └─
par    └────┘                    └─┘                           └─
pid                             └─┘                           
st   ──────────────────────────────────────────────────────────────
405  
src  
typ  
doc  
txt  
par  
pid  
st   
406  def sign_aux2 : list α → perm α → units ℤ
id                   └──┘   └──┘    └───┘ 
src                  └──┘     └──┘     └───┘ 
typ                  └──┘   └──┘    └───┘ 
doc                           └──┘
407  | []     f := 1
id     └┘
src    └┘
typ    └┘
408  | (x::l) f := if x = f x then sign_aux2 l f else -sign_aux2 l (swap x (f x) * f)
id      └┘                     └───────┘          └───────┘    └──┘         
src      └┘                                                       └──┘         
typ     └┘                     └───────┘          └───────┘    └──┘         
doc                                                                 └──┘
409  
410  lemma sign_aux_eq_sign_aux2 {n : ℕ} : ∀ (l : list α) (f : perm α) (e : α ≃ fin n)
id                                              └──┘        └──┘          └─┘ 
src                                              └──┘         └──┘            └─┘
typ                                             └──┘        └──┘          └─┘ 
doc                                                            └──┘           
411    (h : ∀ x, f x ≠ x → x ∈ l), sign_aux ((e.symm.trans f).trans e) = sign_aux2 l f
id                         └──────┘   └───┘└────┘  └───┘     └───────┘  
src                              └──────┘    └───┘└────┘   └───┘      └───────┘
typ                        └──────┘   └───┘└────┘  └───┘     └───────┘  
412  | []     f e h := have f = 1, from equiv.ext _ _ $
id     └┘                            └───────┘
src    └┘                              └───────┘
typ    └┘                            └───────┘
413    λ y, not_not.1 (mt (h y) (list.not_mem_nil _)),
id         └─────┘   └┘       └──────────────┘
src         └─────┘   └┘        └──────────────┘
typ        └─────┘   └┘       └──────────────┘
414  by rw [this, one_def, equiv.trans_refl, equiv.symm_trans, ← one_def,
id          └──┘  └─────┘  └──────────────┘  └──────────────┘    └─────┘
src     └──┘    └┘└─────┘└┘└──────────────┘└┘└──────────────┘└──┘└─────┘└─
typ     └──┘└──┘└┘└─────┘└┘└──────────────┘└┘└──────────────┘└──┘└─────┘└─
doc     └──┘    └┘       └┘                └┘                └──┘       └─
txt     └──┘    └┘       └┘                └┘                └──┘       └─
par     └──┘    └┘       └┘                └┘                └──┘       └─
pid       └┘    └┘       └┘                └┘                └──┘       └─
st     └───────┘└───────┘└────────────────┘└────────────────┘└─────────┘└─
415    sign_aux_one, sign_aux2]
id     └──────────┘  └───────┘
src  ─┘└──────────┘└┘└───────┘└┘
typ  ─┘└──────────┘└┘└───────┘└┘
doc  ─┘            └┘         └┘
txt  ─┘            └┘         └┘
par  ─┘            └┘         └┘
pid  ─┘            └┘         
st   ─────────────┘└─────────┘
416  | (x::l) f e h := begin
id       └┘
src      └┘
typ      └┘
st                     └─────
417    rw sign_aux2,
id        └───────┘
src    └─┘└───────┘
typ    └─┘└───────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ─────────────┘└─
418    by_cases hfx : x = f x,
id                        
src    └───────┘   └─┘  
typ    └───────┘   └─┘ 
doc    └───────┘   └─┘   
txt    └───────┘   └─┘   
par    └───────┘   └─┘   
pid               └─┘   
st   ───────────────────────┘└─
419    { rw if_pos hfx,
id          └────┘ └─┘
src      └─┘└────┘
typ      └─┘└────┘└─┘
doc      └─┘      
txt      └─┘      
par      └─┘      
pid              
st   ───┘└───────────┘└─
420      exact sign_aux_eq_sign_aux2 l f _ (λ y (hy : f y ≠ y), list.mem_of_ne_of_mem
id             └───────────────────┘                         └───────────────────┘
src      └────┘                       └─┘  └───────┘   └─┘└───────────────────┘
typ      └────┘└───────────────────┘ └─┘  └───────┘  └─┘└───────────────────┘
doc      └────┘                       └─┘  └───────┘    └─┘                     
txt      └────┘                       └─┘  └───────┘    └─┘                     
par      └────┘                       └─┘  └───────┘    └─┘                     
pid                                  └─┘  └───────┘    └─┘                     
st   ─────────────────────────────────────────────────────────────────────────────────
421        (λ h : y = x, by simpa [h, hfx.symm] using hy) (h y hy) ) },
id                                                 └┘   
src  ─────┘  └───┘   └┘  └─────┘ └┘        └──────┘  └┘     └──┘
typ  ─────┘  └───┘ └┘  └─────┘└┘└──────┘└──────┘└┘└┘    └──┘
doc  ─────┘  └───┘   └┘  └─────┘ └┘        └──────┘  └┘     └──┘
txt  ─────┘  └───┘   └┘  └─────┘ └┘        └──────┘  └┘     └──┘
par  ─────┘  └───┘   └┘  └─────┘ └┘        └──────┘  └┘     └──┘
pid  ─────┘  └───┘   └┘  └──────┘ └┘        └──────┘  └┘     └─┘
st   ─────────────────────┘└───────────────────────────┘└───────────┘└┘
422    { have hy : ∀ y : α, (swap x (f x) * f) y ≠ y → y ∈ l,
id                          └──┘                     
src      └────────┘ └───┘   └──┘    └┘ └┘     
typ      └────────┘ └───┘  └──┘   └┘└┘    
doc      └────────┘ └───┘   └──┘    └┘  └┘      
txt      └────────┘ └───┘           └┘  └┘      
par      └────────┘ └───┘           └┘  └┘      
pid      └─────┘└─┘ └───┘           └┘  └┘      
st   ──────────────────────────────────────────────────────┘└─
423        from λ y hy, have f y ≠ y ∧ y ≠ x, from ne_and_ne_of_swap_mul_apply_ne_self hy,
id                                               └─────────────────────────────────┘
src        └───┘ └─────┘    └─┘      └─────┘└─────────────────────────────────┘  └─
typ        └───┘ └─────┘    └─┘     └─────┘└─────────────────────────────────┘  └─
doc        └───┘ └─────┘    └─┘       └─────┘                                     └─
txt        └───┘ └─────┘    └─┘       └─────┘                                     └─
par        └───┘ └─────┘    └─┘       └─────┘                                     └─
pid        └───┘ └─────┘    └─┘       └─────┘                                     └─
st   ──────────────────────────────────────────────────────────────────────────────────────
424        list.mem_of_ne_of_mem this.2 (h _ this.1),
id         └───────────────────┘         
src  ─────┘└───────────────────┘    └─┘  └─┘    └─┘
typ  ─────┘└───────────────────┘    └─┘ └─┘    └─┘
doc  ─────┘                         └─┘  └─┘    └─┘
txt  ─────┘                         └─┘  └─┘    └─┘
par  ─────┘                         └─┘  └─┘    └─┘
pid  ─────┘                         └─┘  └─┘    └─┘
st   ──────────────────────────────────────────────┘└─
425      have : (e.symm.trans (swap x (f x) * f)).trans e =
src      └─────┘                      └┘  └───────┘  
typ      └─────┘                      └┘  └───────┘  
doc      └─────┘                      └┘  └───────┘  
txt      └─────┘                      └┘  └───────┘  
par      └─────┘                      └┘  └───────┘  
pid      └───┘└┘                      └┘  └───────┘  
st   ───────────────────────────────────────────────────────
426        (swap (e x) (e (f x))) * (e.symm.trans f).trans e,
id          └──┘                    └──────────┘         
src  ─────┘ └──┘   └┘     └──┘  └──────────┘ └──────┘
typ  ─────┘ └──┘   └┘    └──┘  └──────────┘└──────┘
doc  ─────┘ └──┘   └┘     └──┘               └──────┘
txt  ─────┘        └┘     └──┘               └──────┘
par  ─────┘        └┘     └──┘               └──────┘
pid  ─────┘        └┘     └──┘               └──────┘
st   ──────────────────────────────────────────────────────┘└─
427        from equiv.ext _ _ (λ z, by rw ← equiv.symm_trans_swap_trans; simp [mul_def]),
id              └───────┘                   └─────────────────────────┘        └─────┘
src        └───┘└───────┘└───┘  └──┘  └───┘└─────────────────────────┘└┘└────┘└─────┘
typ        └───┘└───────┘└───┘  └──┘  └───┘└─────────────────────────┘└┘└────┘└─────┘
doc        └───┘         └───┘  └──┘  └───┘                           └┘└────┘       
txt        └───┘         └───┘  └──┘  └───┘                           └┘└────┘       
par        └───┘         └───┘  └──┘  └───┘                           └┘└────┘       
pid        └───┘         └───┘  └──┘  └────┘                           └──────┘       └┘
st   ────────────────────────────────┘└───────────────────────────────────────────────┘└─
428      have hefx : e x ≠ e (f x), from mt (injective.eq_iff e.injective).1 hfx,
id                                    └┘  └──────────────┘ └─────────┘    └─┘
src      └──────────┘         └───┘└┘ └──────────────┘└─────────┘└──┘
typ      └──────────┘      └───┘└┘ └──────────────┘└─────────┘└──┘└─┘
doc      └──────────┘         └───┘                              └──┘
txt      └──────────┘         └───┘                              └──┘
par      └──────────┘         └───┘                              └──┘
pid      └───────┘└─┘         └───┘                              └──┘
st   ────────────────────────────┘└────────────────────────────────────────────┘└─
429      rw [if_neg hfx, ← sign_aux_eq_sign_aux2 _ _ e hy, this, sign_aux_mul, sign_aux_swap hefx],
id           └────┘ └─┘    └───────────────────┘      └┘  └──┘  └──────────┘  └───────────┘ └──┘
src      └──┘└────┘   └──┘                     └───┘   └┘    └┘└──────────┘└┘└───────────┘    
typ      └──┘└────┘└─┘└──┘└───────────────────┘└───┘└┘└┘└──┘└┘└──────────┘└┘└───────────┘└──┘
doc      └──┘         └──┘                     └───┘   └┘    └┘            └┘                 
txt      └──┘         └──┘                     └───┘   └┘    └┘            └┘                 
par      └──┘         └──┘                     └───┘   └┘    └┘            └┘                 
pid        └┘         └──┘                     └───┘   └┘    └┘            └┘                 
st   ─────────────────┘└────────────────────────────────┘└────┘└────────────┘└──────────────────┘└──
430      simp }
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└─
431  end
st   ──┘
432  
433  def sign_aux3 [fintype α] (f : perm α) {s : multiset α} : (∀ x, x ∈ s) → units ℤ :=
id                  └─────┘        └──┘        └──────┘                └───┘ 
src                 └─────┘         └──┘         └──────┘                    └───┘ 
typ                 └─────┘        └──┘        └──────┘                └───┘ 
doc                 └─────┘         └──┘         └──────┘
434  quotient.hrec_on s (λ l h, sign_aux2 l f)
id   └──────────────┘        └───────┘  
src  └──────────────┘           └───────┘
typ  └──────────────┘        └───────┘  
435    (trunc.induction_on (equiv_fin α)
id      └────────────────┘  └───────┘ 
src     └────────────────┘  └───────┘
typ     └────────────────┘  └───────┘ 
doc                         └───────┘
436      (λ e l₁ l₂ h, function.hfunext
id           └┘ └┘   └──────────────┘
src                    └──────────────┘
typ          └┘ └┘   └──────────────┘
437        (show (∀ x, x ∈ l₁) = ∀ x, x ∈ l₂, by simp [list.mem_of_perm h])
id                      └┘         └┘           └──────────────┘ 
src                                           └────┘└──────────────┘ 
typ                     └┘         └┘     └────┘└──────────────┘
doc                                              └────┘                 
txt                                              └────┘                 
par                                              └────┘                 
pid                                                                   
st                                              └────────────────────────┘
438        (λ h₁ h₂ _, by rw [← sign_aux_eq_sign_aux2 _ _ e (λ _ _, h₁ _),
id            └┘ └┘            └───────────────────┘              └┘
src                       └────┘└───────────────────┘└───┘   └────┘  └────
typ           └┘ └┘      └────┘└───────────────────┘└───┘  └────┘└┘└────
doc                       └────┘                     └───┘   └────┘  └────
txt                       └────┘                     └───┘   └────┘  └────
par                       └────┘                     └───┘   └────┘  └────
pid                         └──┘                     └───┘   └────┘  └────
st                       └──────────────────────────────────────────────┘└─
439          ← sign_aux_eq_sign_aux2 _ _ e (λ _ _, h₂ _)])))
id             └───────────────────┘              └┘
src  ─────────┘└───────────────────┘└───┘   └────┘  └──┘
typ  ─────────┘└───────────────────┘└───┘  └────┘└┘└──┘
doc  ─────────┘                     └───┘   └────┘  └──┘
txt  ─────────┘                     └───┘   └────┘  └──┘
par  ─────────┘                     └───┘   └────┘  └──┘
pid  ─────────┘                     └───┘   └────┘  └──┘
st   ──────────────────────────────────────────────────┘
440  
441  lemma sign_aux3_mul_and_swap [fintype α] (f g : perm α) (s : multiset α) (hs : ∀ x, x ∈ s) :
id                                 └─────┘          └──┘        └──────┘               
src                                └─────┘           └──┘         └──────┘                 
typ                                └─────┘          └──┘        └──────┘               
doc                                └─────┘           └──┘         └──────┘
442    sign_aux3 (f * g) hs = sign_aux3 f hs * sign_aux3 g hs ∧ ∀ x y, x ≠ y →
id     └───────┘      └┘  └───────┘  └┘  └───────┘  └┘         
src    └───────┘            └───────┘       └───────┘                
typ    └───────┘      └┘  └───────┘  └┘  └───────┘  └┘         
443    sign_aux3 (swap x y) hs = -1 :=
id     └───────┘  └──┘    └┘  
src    └───────┘  └──┘          
typ    └───────┘  └──┘    └┘  
doc               └──┘
444  let ⟨l, hl⟩ := quotient.exists_rep s in
id   └─┘            └─────────────────┘ 
src                 └─────────────────┘
typ  └─┘            └─────────────────┘ 
445  let ⟨e, _⟩ := trunc.exists_rep (equiv_fin α) in
id   └─┘           └──────────────┘  └───────┘ 
src                └──────────────┘  └───────┘
typ  └─┘           └──────────────┘  └───────┘ 
doc                                  └───────┘
446  begin
st   └─────
447    clear _let_match _let_match,
src    └─────────────────────────┘
typ    └─────────────────────────┘
doc    └─────────────────────────┘
txt    └─────────────────────────┘
par    └─────────────────────────┘
pid         └────────────────────┘
st   ────────────────────────────┘└─
448    subst hl,
id           └┘
src    └────┘
typ    └────┘└┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────┘└─
449    show sign_aux2 l (f * g) = sign_aux2 l f * sign_aux2 l g ∧
id                                                         
src    └───┘             └┘                        
typ    └───┘             └┘                      
doc    └───┘              └┘                         
txt    └───┘              └┘                         
par    └───┘              └┘                         
pid    └───┘              └┘                         
st   ─────────────────────────────────────────────────────────────
450      ∀ x y, x ≠ y → sign_aux2 l (swap x y) = -1,
id                     └───────┘   └──┘        
src  ───┘ └──┘    └───────┘  └──┘  └┘ 
typ  ───┘ └──┘    └───────┘ └──┘  └┘ 
doc  ───┘ └──┘                └──┘  └┘  
txt  ───┘ └──┘                      └┘  
par  ───┘ └──┘                      └┘  
pid  ───┘ └──┘                      └┘  
st   ─────────────────────────────────────────────┘└─
451    have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e,
id                                                                            └──────────┘         
src    └─────────┘                 └───────┘                └──────┘   └──────────┘ └──────┘
typ    └─────────┘                 └───────┘               └──────┘   └──────────┘└──────┘
doc    └─────────┘                 └───────┘                └──────┘                └──────┘
txt    └─────────┘                 └───────┘                └──────┘                └──────┘
par    └─────────┘                 └───────┘                └──────┘                └──────┘
pid    └──────┘└─┘                 └───────┘                └──────┘                └──────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
452      from equiv.ext _ _ (λ h, by simp [mul_apply]),
id            └───────┘                    └───────┘
src      └───┘└───────┘└───┘  └──┘  └────┘└───────┘
typ      └───┘└───────┘└───┘  └──┘  └────┘└───────┘
doc      └───┘         └───┘  └──┘  └────┘         
txt      └───┘         └───┘  └──┘  └────┘         
par      └───┘         └───┘  └──┘  └────┘         
pid      └───┘         └───┘  └──┘  └─────┘         └┘
st   ──────────────────────────────┘└───────────────┘└─
453    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
454    { rw [← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), ← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _),
id             └───────────────────┘              └┘       └───────────────────┘              └┘
src      └────┘└───────────────────┘└───┘   └────┘  └─────┘└───────────────────┘└───┘   └────┘  └────
typ      └────┘└───────────────────┘└───┘  └────┘└┘└─────┘└───────────────────┘└───┘  └────┘└┘└────
doc      └────┘                     └───┘   └────┘  └─────┘                     └───┘   └────┘  └────
txt      └────┘                     └───┘   └────┘  └─────┘                     └───┘   └────┘  └────
par      └────┘                     └───┘   └────┘  └─────┘                     └───┘   └────┘  └────
pid        └──┘                     └───┘   └────┘  └─────┘                     └───┘   └────┘  └────
st   ───┘└─────────────────────────────────────────────┘└───────────────────────────────────────────┘└─
455        ← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), hfg, sign_aux_mul] },
id           └───────────────────┘              └┘     └─┘  └──────────┘
src  ───────┘└───────────────────┘└───┘   └────┘  └───┘   └┘└──────────┘└┘
typ  ───────┘└───────────────────┘└───┘  └────┘└┘└───┘└─┘└┘└──────────┘└┘
doc  ───────┘                     └───┘   └────┘  └───┘   └┘            └┘
txt  ───────┘                     └───┘   └────┘  └───┘   └┘            └┘
par  ───────┘                     └───┘   └────┘  └───┘   └┘            └┘
pid  ───────┘                     └───┘   └────┘  └───┘   └┘            
st   ────────────────────────────────────────────────┘└───┘└────────────┘└┘
456    { assume x y hxy,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid      └────────────┘
st   ─────────────────┘└─
457      have hexy : e x ≠ e y, from mt (injective.eq_iff e.injective).1 hxy,
id                                └┘  └──────────────┘ └─────────┘    └─┘
src      └──────────┘       └───┘└┘ └──────────────┘└─────────┘└──┘
typ      └──────────┘    └───┘└┘ └──────────────┘└─────────┘└──┘└─┘
doc      └──────────┘       └───┘                              └──┘
txt      └──────────┘       └───┘                              └──┘
par      └──────────┘       └───┘                              └──┘
pid      └───────┘└─┘       └───┘                              └──┘
st   ────────────────────────┘└────────────────────────────────────────────┘└─
458      rw [← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), equiv.symm_trans_swap_trans, sign_aux_swap hexy] }
id             └───────────────────┘              └┘     └─────────────────────────┘  └───────────┘ └──┘
src      └────┘└───────────────────┘└───┘   └────┘  └───┘└─────────────────────────┘└┘└───────────┘    └┘
typ      └────┘└───────────────────┘└───┘  └────┘└┘└───┘└─────────────────────────┘└┘└───────────┘└──┘└┘
doc      └────┘                     └───┘   └────┘  └───┘                           └┘                 └┘
txt      └────┘                     └───┘   └────┘  └───┘                           └┘                 └┘
par      └────┘                     └───┘   └────┘  └───┘                           └┘                 └┘
pid        └──┘                     └───┘   └────┘  └───┘                           └┘                 
st   ──────────────────────────────────────────────────┘└───────────────────────────┘└──────────────────┘└─
459  end
st   ──┘
460  
461  /-- `sign` of a permutation returns the signature or parity of a permutation, `1` for even
462  permutations, `-1` for odd permutations. It is the unique surjective group homomorphism from
463  `perm α` to the group with two elements.-/
464  def sign [fintype α] (f : perm α) := sign_aux3 f mem_univ
id             └─────┘        └──┘      └───────┘  └──────┘
src            └─────┘         └──┘       └───────┘   └──────┘
typ            └─────┘        └──┘      └───────┘  └──────┘
doc            └─────┘         └──┘
465  
466  instance sign.is_group_hom [fintype α] : is_group_hom (@sign α _ _) :=
id                               └─────┘     └──────────┘   └──┘ 
src                              └─────┘      └──────────┘   └──┘
typ                              └─────┘     └──────────┘   └──┘ 
doc                              └─────┘      └──────────┘   └──┘
467  { map_mul := λ f g, (sign_aux3_mul_and_swap f g _ mem_univ).1 }
id                      └────────────────────┘     └──────┘ 
src                       └────────────────────┘       └──────┘ 
typ                     └────────────────────┘     └──────┘ 
468  
469  section sign
470  
471  variable [fintype α]
id             └─────┘
src            └─────┘
typ            └─────┘
doc            └─────┘
472  
473  @[simp] lemma sign_mul (f g : perm α) : sign (f * g) = sign f * sign g :=
id                                 └──┘     └──┘       └──┘   └──┘ 
src                                └──┘      └──┘         └──┘    └──┘
typ                                └──┘     └──┘       └──┘   └──┘ 
doc    └──┘                        └──┘      └──┘           └──┘     └──┘
474  is_mul_hom.map_mul sign _ _
id   └────────────────┘ └──┘
src  └────────────────┘ └──┘
typ  └────────────────┘ └──┘
doc                     └──┘
475  
476  @[simp] lemma sign_one : (sign (1 : perm α)) = 1 :=
id                             └──┘      └──┘    
src                            └──┘      └──┘     
typ                            └──┘      └──┘    
doc    └──┘                    └──┘      └──┘
477  is_group_hom.map_one sign
id   └──────────────────┘ └──┘
src  └──────────────────┘ └──┘
typ  └──────────────────┘ └──┘
doc  └──────────────────┘ └──┘
478  
479  @[simp] lemma sign_refl : sign (equiv.refl α) = 1 :=
id                             └──┘  └────────┘   
src                            └──┘  └────────┘    
typ                            └──┘  └────────┘   
doc    └──┘                    └──┘
480  is_group_hom.map_one sign
id   └──────────────────┘ └──┘
src  └──────────────────┘ └──┘
typ  └──────────────────┘ └──┘
doc  └──────────────────┘ └──┘
481  
482  @[simp] lemma sign_inv (f : perm α) : sign f⁻¹ = sign f :=
id                               └──┘     └──┘ └┘  └──┘ 
src                              └──┘      └──┘  └┘  └──┘
typ                              └──┘     └──┘ └┘  └──┘ 
doc    └──┘                      └──┘      └──┘       └──┘
483  by rw [is_group_hom.map_inv sign, int.units_inv_eq_self]; apply_instance
id          └──────────────────┘ └──┘  └───────────────────┘
src     └──┘└──────────────────┘└──┘└┘└───────────────────┘  └──────────────
typ     └──┘└──────────────────┘└──┘└┘└───────────────────┘  └──────────────
doc     └──┘└──────────────────┘└──┘└┘                       └──────────────
txt     └──┘                        └┘                       └──────────────
par     └──┘                        └┘                       └──────────────
pid       └┘                        └┘                                     
st     └────────────────────────────┘└─────────────────────┘└────────────────
484  
src  
typ  
doc  
txt  
par  
pid  
st   
485  lemma sign_swap {x y : α} (h : x ≠ y) : sign (swap x y) = -1 :=
id                                       └──┘  └──┘     
src                                         └──┘  └──┘       
typ                                      └──┘  └──┘     
doc                                          └──┘  └──┘
486  (sign_aux3_mul_and_swap 1 1 _ mem_univ).2 x y h
id    └────────────────────┘       └──────┘     
src   └────────────────────┘       └──────┘ 
typ   └────────────────────┘       └──────┘     
487  
488  @[simp] lemma sign_swap' {x y : α} :
id                                   
typ                                  
doc    └──┘
489    (swap x y).sign = if x = y then 1 else -1 :=
id      └──┘   └──┘                     
src     └──┘     └──┘                       
typ     └──┘   └──┘                     
doc     └──┘     └──┘
490  if H : x = y then by simp [H, swap_self] else
id   └┘                        └───────┘
src  └┘                  └────┘ └┘└───────┘└┘
typ  └┘                └────┘└┘└───────┘└┘
doc                       └────┘ └┘         └┘
txt                       └────┘ └┘         └┘
par                       └────┘ └┘         └┘
pid                            └┘         
st                       └───────────────────┘
491  by simp [sign_swap H, H]
id            └───────┘   
src     └────┘└───────┘ └┘ └─
typ     └────┘└───────┘└┘└─
doc     └────┘          └┘ └─
txt     └────┘          └┘ └─
par     └────┘          └┘ └─
pid                   └┘ 
st     └──────────────────────
492  
src  
typ  
doc  
txt  
par  
pid  
st   
493  lemma sign_eq_of_is_swap {f : perm α} (h : is_swap f) : sign f = -1 :=
id                                 └──┘        └─────┘     └──┘   
src                                └──┘         └─────┘      └──┘    
typ                                └──┘        └─────┘     └──┘   
doc                                └──┘                      └──┘
494  let ⟨x, y, hxy⟩ := h in hxy.2.symm ▸ sign_swap hxy.1
id   └─┘        └─┘             └──┘   └───────┘    
src                              └──┘   └───────┘    
typ  └─┘        └─┘             └──┘   └───────┘    
495  
496  lemma sign_aux3_symm_trans_trans [decidable_eq β] [fintype β] (f : perm α)
id                                     └──────────┘    └─────┘        └──┘ 
src                                    └──────────┘     └─────┘         └──┘
typ                                    └──────────┘    └─────┘        └──┘ 
doc                                                     └─────┘         └──┘
497    (e : α ≃ β) {s : multiset α} {t : multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) :
id                   └──────┘        └──────┘                             
src                    └──────┘         └──────┘                                  
typ                  └──────┘        └──────┘                             
doc                    └──────┘         └──────┘
498    sign_aux3 ((e.symm.trans f).trans e) ht = sign_aux3 f hs :=
id     └───────┘   └───┘└────┘  └───┘    └┘  └───────┘  └┘
src    └───────┘    └───┘└────┘   └───┘         └───────┘
typ    └───────┘   └───┘└────┘  └───┘    └┘  └───────┘  └┘
499  quotient.induction_on₂ t s
id   └────────────────────┘  
src  └────────────────────┘
typ  └────────────────────┘  
500    (λ l₁ l₂ h₁ h₂, show sign_aux2 _ _ = sign_aux2 _ _,
id        └┘ └┘ └┘ └┘       └───────┘      └───────┘
src                         └───────┘      └───────┘
typ       └┘ └┘ └┘ └┘       └───────┘      └───────┘
501      from let n := trunc.out (equiv_fin β) in
id                    └───────┘  └───────┘ 
src                    └───────┘  └───────┘
typ                   └───────┘  └───────┘ 
doc                    └───────┘  └───────┘
502      by rw [← sign_aux_eq_sign_aux2 _ _ n (λ _ _, h₁ _),
id                └───────────────────┘              └┘
src         └────┘└───────────────────┘└───┘   └────┘  └────
typ         └────┘└───────────────────┘└───┘  └────┘└┘└────
doc         └────┘                     └───┘   └────┘  └────
txt         └────┘                     └───┘   └────┘  └────
par         └────┘                     └───┘   └────┘  └────
pid           └──┘                     └───┘   └────┘  └────
st         └──────────────────────────────────────────────┘└─
503          ← sign_aux_eq_sign_aux2 _ _ (e.trans n) (λ _ _, h₂ _)];
id             └───────────────────┘      └─────┘           └┘
src  ─────────┘└───────────────────┘└───┘ └─────┘ └┘  └────┘  └──┘
typ  ─────────┘└───────────────────┘└───┘ └─────┘└┘  └────┘└┘└──┘
doc  ─────────┘                     └───┘         └┘  └────┘  └──┘
txt  ─────────┘                     └───┘         └┘  └────┘  └──┘
par  ─────────┘                     └───┘         └┘  └────┘  └──┘
pid  ─────────┘                     └───┘         └┘  └────┘  └──┘
st   ────────────────────────────────────────────────────────────┘└─
504        exact congr_arg sign_aux (equiv.ext _ _ (λ x, by simp)))
id               └───────┘ └──────┘  └───────┘
src        └────┘└───────┘└──────┘ └───────┘└───┘  └──┘  └──┘└┘
typ        └────┘└───────┘└──────┘ └───────┘└───┘  └──┘  └──┘└┘
doc        └────┘                           └───┘  └──┘  └──┘└┘
txt        └────┘                           └───┘  └──┘  └──┘└┘
par        └────┘                           └───┘  └──┘  └──┘└┘
pid                                        └───┘  └──┘  └─────┘
st   ─────────────────────────────────────────────────────┘└───┘└┘
505    ht hs
id     └┘ └┘
typ    └┘ └┘
506  
507  lemma sign_symm_trans_trans [decidable_eq β] [fintype β] (f : perm α)
id                                └──────────┘    └─────┘        └──┘ 
src                               └──────────┘     └─────┘         └──┘
typ                               └──────────┘    └─────┘        └──┘ 
doc                                                └─────┘         └──┘
508    (e : α ≃ β) : sign ((e.symm.trans f).trans e) = sign f :=
id                └──┘   └───┘└────┘  └───┘     └──┘ 
src                 └──┘    └───┘└────┘   └───┘      └──┘
typ               └──┘   └───┘└────┘  └───┘     └──┘ 
doc                 └──┘                              └──┘
509  sign_aux3_symm_trans_trans f e mem_univ mem_univ
id   └────────────────────────┘   └──────┘ └──────┘
src  └────────────────────────┘     └──────┘ └──────┘
typ  └────────────────────────┘   └──────┘ └──────┘
510  
511  lemma sign_prod_list_swap {l : list (perm α)}
id                                  └──┘  └──┘ 
src                                 └──┘  └──┘
typ                                 └──┘  └──┘ 
doc                                       └──┘
512    (hl : ∀ g ∈ l, is_swap g) : sign l.prod = -1 ^ l.length :=
id                  └─────┘     └──┘ └───┘     └─────┘
src                   └─────┘      └──┘  └───┘      └─────┘
typ                 └─────┘     └──┘ └───┘     └─────┘
doc                                └──┘  └───┘
513  have h₁ : l.map sign = list.repeat (-1) l.length :=
id             └──┘ └──┘  └─────────┘     └─────┘
src             └──┘ └──┘  └─────────┘      └─────┘
typ            └──┘ └──┘  └─────────┘     └─────┘
doc                  └──┘
514    list.eq_repeat.2 ⟨by simp, λ u hu,
id     └────────────┘               └┘
src    └────────────┘      └──┘
typ    └────────────┘      └──┘     └┘
doc                         └──┘
txt                         └──┘
par                         └──┘
st                         └───┘
515    let ⟨g, hg⟩ := list.mem_map.1 hu in
id     └─┘     └┘     └──────────┘  └┘
src                   └──────────┘
typ    └─┘     └┘     └──────────┘  └┘
516    hg.2 ▸ sign_eq_of_is_swap (hl _ hg.1)⟩,
id          └────────────────┘  └┘     
src         └────────────────┘         
typ         └────────────────┘  └┘     
517  by rw [← list.prod_repeat, ← h₁, list.prod_hom _ (@sign α _ _)]
id            └──────────────┘    └┘  └───────────┘     └──┘ 
src     └────┘└──────────────┘└──┘  └┘└───────────┘└─┘  └──┘ └──────
typ     └────┘└──────────────┘└──┘└┘└┘└───────────┘└─┘  └──┘└──────
doc     └────┘                └──┘  └┘             └─┘  └──┘ └──────
txt     └────┘                └──┘  └┘             └─┘       └──────
par     └────┘                └──┘  └┘             └─┘       └──────
pid       └──┘                └──┘  └┘             └─┘       └────┘
st     └─────────────────────┘└────┘└─────────────────────────────┘
518  
src  
typ  
doc  
txt  
par  
pid  
st   
519  lemma sign_surjective (hα : 1 < fintype.card α) : function.surjective (sign : perm α → units ℤ) :=
id                                  └──────────┘     └─────────────────┘  └──┘   └──┘    └───┘ 
src                                 └──────────┘      └─────────────────┘  └──┘   └──┘     └───┘ 
typ                                 └──────────┘     └─────────────────┘  └──┘   └──┘    └───┘ 
doc                                  └──────────┘                           └──┘   └──┘
520  λ a, (int.units_eq_one_or a).elim
id        └─────────────────┘  └──┘
src        └─────────────────┘   └──┘
typ       └─────────────────┘  └──┘
521    (λ h, ⟨1, by simp [h]⟩)
id                       
src                 └────┘ 
typ                └────┘
doc                 └────┘ 
txt                 └────┘ 
par                 └────┘ 
pid                      
st                 └───────┘
522    (λ h, let ⟨x⟩ := fintype.card_pos_iff.1 (lt_trans zero_lt_one hα) in
id          └─┘       └──────────────────┘   └──────┘ └─────────┘ └┘
src                     └──────────────────┘   └──────┘ └─────────┘
typ         └─┘       └──────────────────┘   └──────┘ └─────────┘ └┘
523      let ⟨y, hxy⟩ := fintype.exists_ne_of_one_lt_card hα x in
id       └─┘            └──────────────────────────────┘ └┘
src                      └──────────────────────────────┘
typ      └─┘            └──────────────────────────────┘ └┘
524      ⟨swap y x, by rw [sign_swap hxy, h]⟩ )
id        └──┘             └───────┘ └─┘  
src       └──┘         └──┘└───────┘   └┘ 
typ       └──┘         └──┘└───────┘└─┘└┘
doc       └──┘         └──┘            └┘ 
txt                    └──┘            └┘ 
par                    └──┘            └┘ 
pid                      └┘            └┘ 
st                    └────────────────┘└─┘
525  
526  lemma eq_sign_of_surjective_hom {s : perm α → units ℤ}
id                                        └──┘    └───┘ 
src                                       └──┘     └───┘ 
typ                                       └──┘    └───┘ 
doc                                       └──┘
527    [is_group_hom s] (hs : surjective s) : s = sign :=
id      └──────────┘         └────────┘       └──┘
src     └──────────┘          └────────┘         └──┘
typ     └──────────┘         └────────┘       └──┘
doc     └──────────┘                              └──┘
528  have ∀ {f}, is_swap f → s f = -1 :=
id              └─────┘       
src              └─────┘          
typ             └─────┘       
529    λ f ⟨x, y, hxy, hxy'⟩, hxy'.symm ▸ by_contradiction (λ h,
id                   └──┘       └───┘  └──────────────┘    
src                               └───┘  └──────────────┘
typ                  └──┘       └───┘  └──────────────┘    
530      have ∀ f, is_swap f → s f = 1 := λ f ⟨a, b, hab, hab'⟩,
id                └─────┘               
src                └─────┘         
typ               └─────┘               
531        by rw [← is_conj_iff_eq, ← or.resolve_right (int.units_eq_one_or _) h, hab'];
id                  └────────────┘    └──────────────┘  └─────────────────┘      └──┘
src           └────┘└────────────┘└──┘└──────────────┘ └─────────────────┘└──┘ └┘    
typ           └────┘└────────────┘└──┘└──────────────┘ └─────────────────┘└──┘└┘└──┘
doc           └────┘              └──┘                                    └──┘ └┘    
txt           └────┘              └──┘                                    └──┘ └┘    
par           └────┘              └──┘                                    └──┘ └┘    
pid             └──┘              └──┘                                    └──┘ └┘    
st           └───────────────────┘└────────────────────────────────────────────┘└────┘└─
532          exact is_group_hom.is_conj _ (is_conj_swap hab hxy),
id                 └──────────────────┘    └──────────┘ └─┘ └─┘
src          └────┘└──────────────────┘└─┘ └──────────┘      
typ          └────┘└──────────────────┘└─┘ └──────────┘└─┘└─┘
doc          └────┘                    └─┘                   
txt          └────┘                    └─┘                   
par          └────┘                    └─┘                   
pid                                   └─┘                   
st   ──────────────────────────────────────────────────────────┘
533    let ⟨g, hg⟩ := hs (-1) in
id     └─┘           └┘  
src                       
typ    └─┘           └┘  
534    let ⟨l, hl⟩ := trunc.out (trunc_swap_factors g) in
id     └─┘    └┘     └───────┘  └────────────────┘
src                   └───────┘  └────────────────┘
typ    └─┘    └┘     └───────┘  └────────────────┘
doc                   └───────┘
535    have ∀ a ∈ l.map s, a = (1 : units ℤ) := λ a ha,
id                └──┘          └───┘         └┘
src                └──┘            └───┘ 
typ               └──┘          └───┘         └┘
536      let ⟨g, hg⟩ := list.mem_map.1 ha in hg.2 ▸ this _ (hl.2 _ hg.1),
id       └─┘     └┘     └──────────┘  └┘         └──┘            
src                     └──────────┘                             
typ      └─┘     └┘     └──────────┘  └┘         └──┘            
537    have s l.prod = 1,
id            └───┘ 
src            └───┘ 
typ           └───┘ 
doc            └───┘
538      by rw [← l.prod_hom s, list.eq_repeat'.2 this, list.prod_repeat, one_pow],
id                └────────┘   └─────────────┘   └──┘  └──────────────┘  └─────┘
src         └────┘└────────┘ └┘└─────────────┘└─┘    └┘└──────────────┘└┘└─────┘
typ         └────┘└────────┘└┘└─────────────┘└─┘└──┘└┘└──────────────┘└┘└─────┘
doc         └────┘           └┘               └─┘    └┘                └┘       
txt         └────┘           └┘               └─┘    └┘                └┘       
par         └────┘           └┘               └─┘    └┘                └┘       
pid           └──┘           └┘               └─┘    └┘                └┘       
st         └─────────────────┘└──────────────────────┘└────────────────┘└───────┘
539    by rw [hl.1, hg] at this;
id            └┘    └┘
src       └──┘  └──┘  └───────┘
typ       └──┘└┘└──┘└┘└───────┘
doc       └──┘  └──┘  └───────┘
txt       └──┘  └──┘  └───────┘
par       └──┘  └──┘  └───────┘
pid         └┘  └──┘  └──────┘
st       └─────┘└────┘└─────────
540      exact absurd this dec_trivial),
id             └────┘ └──┘ └─────────┘
src      └────┘└────┘    └─────────┘
typ      └────┘└────┘└──┘└─────────┘
doc      └────┘          └─────────┘
txt      └────┘          
par      └────┘          
pid                     
st   ────────────────────────────────┘
541  funext $ λ f,
id   └────┘     
src  └────┘
typ  └────┘     
542  let ⟨l, hl₁, hl₂⟩ := trunc.out (trunc_swap_factors f) in
id   └─┘         └─┘     └───────┘  └────────────────┘ 
src                       └───────┘  └────────────────┘
typ  └─┘         └─┘     └───────┘  └────────────────┘ 
doc                       └───────┘
543  have hsl : ∀ a ∈ l.map s, a = (-1 : units ℤ) := λ a ha,
id                    └──┘          └───┘         └┘
src                    └──┘            └───┘ 
typ                   └──┘          └───┘         └┘
544    let ⟨g, hg⟩ := list.mem_map.1 ha in hg.2 ▸  this (hl₂ _ hg.1),
id     └─┘     └┘     └──────────┘  └┘          └──┘          
src                   └──────────┘                            
typ    └─┘     └┘     └──────────┘  └┘          └──┘          
545  by rw [← hl₁, ← l.prod_hom s, list.eq_repeat'.2 hsl, list.length_map,
id            └─┘    └────────┘   └─────────────┘   └─┘  └─────────────┘
src     └────┘   └──┘└────────┘ └┘└─────────────┘└─┘   └┘└─────────────┘└─
typ     └────┘└─┘└──┘└────────┘└┘└─────────────┘└─┘└─┘└┘└─────────────┘└─
doc     └────┘   └──┘           └┘               └─┘   └┘               └─
txt     └────┘   └──┘           └┘               └─┘   └┘               └─
par     └────┘   └──┘           └┘               └─┘   └┘               └─
pid       └──┘   └──┘           └┘               └─┘   └┘               └─
st     └────────┘└──────────────┘└─────────────────────┘└───────────────┘└─
546       list.prod_repeat, sign_prod_list_swap hl₂]
id        └──────────────┘  └─────────────────┘ └─┘
src  ────┘└──────────────┘└┘└─────────────────┘   └─
typ  ────┘└──────────────┘└┘└─────────────────┘└─┘└─
doc  ────┘                └┘                      └─
txt  ────┘                └┘                      └─
par  ────┘                └┘                      └─
pid  ────┘                └┘                      
st   ────────────────────┘└───────────────────────┘
547  
src  
typ  
doc  
txt  
par  
pid  
st   
548  lemma sign_subtype_perm (f : perm α) {p : α → Prop} [decidable_pred p]
id                                └──┘                  └────────────┘ 
src                               └──┘                    └────────────┘
typ                               └──┘                  └────────────┘ 
doc                               └──┘
549    (h₁ : ∀ x, p x ↔ p (f x)) (h₂ : ∀ x, f x ≠ x → p x) : sign (subtype_perm f h₁) = sign f :=
id                                             └──┘  └──────────┘  └┘   └──┘ 
src                                                        └──┘  └──────────┘        └──┘
typ                                            └──┘  └──────────┘  └┘   └──┘ 
doc                                                          └──┘                       └──┘
550  let l := trunc.out (trunc_swap_factors (subtype_perm f h₁)) in
id           └───────┘  └────────────────┘  └──────────┘  └┘
src           └───────┘  └────────────────┘  └──────────┘
typ          └───────┘  └────────────────┘  └──────────┘  └┘
doc           └───────┘
551  have hl' : ∀ g' ∈ l.1.map of_subtype, is_swap g' :=
id                └┘    └─┘  └────────┘  └─────┘ └┘
src                      └─┘  └────────┘  └─────┘
typ               └┘    └─┘  └────────┘  └─────┘ └┘
552    λ g' hg',
id       └┘ └─┘
typ      └┘ └─┘
553    let ⟨g, hg⟩ := list.mem_map.1 hg' in
id     └─┘     └┘     └──────────┘  └─┘
src                   └──────────┘
typ    └─┘     └┘     └──────────┘  └─┘
554    hg.2 ▸ is_swap_of_subtype (l.2.2 _ hg.1),
id          └────────────────┘         
src         └────────────────┘          
typ         └────────────────┘         
555  have hl'₂ : (l.1.map of_subtype).prod = f,
id                 └─┘  └────────┘ └──┘   
src                 └─┘  └────────┘ └──┘  
typ                └─┘  └────────┘ └──┘   
doc                                  └──┘
556    by rw [l.1.prod_hom of_subtype, l.2.1, of_subtype_subtype_perm _ h₂],
id                        └────────┘        └─────────────────────┘   └┘
src       └──┘ └──────────┘└────────┘└┘ └────┘└─────────────────────┘└─┘  
typ       └──┘└──────────┘└────────┘└┘└────┘└─────────────────────┘└─┘└┘
doc       └──┘ └──────────┘          └┘ └────┘                       └─┘  
txt       └──┘ └──────────┘          └┘ └────┘                       └─┘  
par       └──┘ └──────────┘          └┘ └────┘                       └─┘  
pid         └┘ └──────────┘          └┘ └────┘                       └─┘  
st       └──────────────────────────┘└───┘└──────────────────────────────┘
557  by conv {congr, rw ← l.2.1, skip, rw ← hl'₂};
id                                         └──┘
src     └────┘└───┘└┘└───┘ └──┘└┘└──┘└┘└───┘    
typ     └────┘└───┘└┘└───┘└──┘└┘└──┘└┘└───┘└──┘
txt     └────┘└───┘└┘└───┘ └──┘└┘└──┘└┘└───┘    
par     └────┘└───┘└┘└───┘ └──┘└┘└──┘└┘└───┘    
pid         └───────────┘ └───────────────┘    
st     └─────┘└───┘└──────────┘└────┘└─────────┘└┘
558    rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', list.length_map]
id         └─────────────────┘       └─────────────────┘ └─┘  └─────────────┘
src    └──┘└─────────────────┘ └────┘└─────────────────┘   └┘└─────────────┘└─
typ    └──┘└─────────────────┘└────┘└─────────────────┘└─┘└┘└─────────────┘└─
doc    └──┘                    └────┘                      └┘               └─
txt    └──┘                    └────┘                      └┘               └─
par    └──┘                    └────┘                      └┘               └─
pid      └┘                    └────┘                      └┘               
st   ─────┘└─────────────────────┘└─────────────────────────┘└───────────────┘
559  
src  
typ  
doc  
txt  
par  
pid  
st   
560  @[simp] lemma sign_of_subtype {p : α → Prop} [decidable_pred p]
id                                                └────────────┘ 
src                                                └────────────┘
typ                                               └────────────┘ 
doc    └──┘
561    (f : perm (subtype p)) : sign (of_subtype f) = sign f :=
id          └──┘  └─────┘      └──┘  └────────┘    └──┘ 
src         └──┘  └─────┘       └──┘  └────────┘     └──┘
typ         └──┘  └─────┘      └──┘  └────────┘    └──┘ 
doc         └──┘                └──┘                  └──┘
562  have ∀ x, of_subtype f x ≠ x → p x, from λ x, not_imp_comm.1 (of_subtype_apply_of_not_mem f),
id            └────────┘                   └──────────┘   └─────────────────────────┘ 
src            └────────┘                         └──────────┘   └─────────────────────────┘
typ           └────────┘                   └──────────┘   └─────────────────────────┘ 
563  by conv {to_rhs, rw [← subtype_perm_of_subtype f, sign_subtype_perm _ _ this]}
id                          └─────────────────────┘   └───────────────┘     └──┘
src     └────┘└────┘└┘└────┘└─────────────────────┘ └┘└───────────────┘└───┘    └─
typ     └────┘└────┘└┘└────┘└─────────────────────┘└┘└───────────────┘└───┘└──┘└─
txt     └────┘└────┘└┘└────┘                        └┘                 └───┘    └─
par     └────┘└────┘└┘└────┘                        └┘                 └───┘    └─
pid         └─────────────┘                        └┘                 └───┘    └┘
st     └─────┘└────┘└───────────────────────────────┘└──────────────────────────┘ 
564  
src  
typ  
txt  
par  
pid  
st   
565  lemma sign_eq_sign_of_equiv [decidable_eq β] [fintype β] (f : perm α) (g : perm β)
id                                └──────────┘    └─────┘        └──┘        └──┘ 
src                               └──────────┘     └─────┘         └──┘         └──┘
typ                               └──────────┘    └─────┘        └──┘        └──┘ 
doc                                                └─────┘         └──┘         └──┘
566    (e : α ≃ β) (h : ∀ x, e (f x) = g (e x)) : sign f = sign g :=
id                                     └──┘   └──┘ 
src                                             └──┘    └──┘
typ                                    └──┘   └──┘ 
doc                                              └──┘     └──┘
567  have hg : g = (e.symm.trans f).trans e, from equiv.ext _ _ $ by simp [h],
id                └───┘└────┘  └───┘         └───────┘                
src                 └───┘└────┘   └───┘          └───────┘          └────┘ 
typ               └───┘└────┘  └───┘         └───────┘          └────┘
doc                                                                  └────┘ 
txt                                                                  └────┘ 
par                                                                  └────┘ 
pid                                                                       
st                                                                  └───────┘
568  by rw [hg, sign_symm_trans_trans]
id          └┘  └───────────────────┘
src     └──┘  └┘└───────────────────┘└─
typ     └──┘└┘└┘└───────────────────┘└─
doc     └──┘  └┘                     └─
txt     └──┘  └┘                     └─
par     └──┘  └┘                     └─
pid       └┘  └┘                     
st     └─────┘└─────────────────────┘
569  
src  
typ  
doc  
txt  
par  
pid  
st   
570  lemma sign_bij [decidable_eq β] [fintype β]
id                   └──────────┘    └─────┘ 
src                  └──────────┘     └─────┘
typ                  └──────────┘    └─────┘ 
doc                                   └─────┘
571    {f : perm α} {g : perm β} (i : Π x : α, f x ≠ x → β)
id          └──┘        └──┘                      
src         └──┘         └──┘                      
typ         └──┘        └──┘                      
doc         └──┘         └──┘
572    (h : ∀ x hx hx', i (f x) hx' = g (i x hx))
id             └┘ └─┘       └─┘      └┘
src                                 
typ            └┘ └─┘       └─┘      └┘
573    (hi : ∀ x₁ x₂ hx₁ hx₂, i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂)
id             └┘ └┘ └─┘ └─┘   └┘ └─┘   └┘ └─┘   └┘  └┘
src                                                   
typ            └┘ └┘ └─┘ └─┘   └┘ └─┘   └┘ └─┘   └┘  └┘
574    (hg : ∀ y, g y ≠ y → ∃ x hx, i x hx = y) :
id                       └┘   └┘  
src                                     
typ                      └┘   └┘  
575    sign f = sign g :=
id     └──┘   └──┘ 
src    └──┘    └──┘
typ    └──┘   └──┘ 
doc    └──┘     └──┘
576  calc sign f = sign (@subtype_perm _ f (λ x, f x ≠ x) (by simp)) :
id        └──┘    └──┘   └──────────┘            
src       └──┘     └──┘   └──────────┘                       └──┘
typ       └──┘    └──┘   └──────────┘                  └──┘
doc       └──┘     └──┘                                       └──┘
txt                                                           └──┘
par                                                           └──┘
st                                                           └───┘
577    eq.symm (sign_subtype_perm _ _ (λ _, id))
id     └─────┘  └───────────────┘          └┘
src    └─────┘  └───────────────┘           └┘
typ    └─────┘  └───────────────┘          └┘
578  ... = sign (@subtype_perm _ g (λ x, g x ≠ x) (by simp)) :
id         └──┘   └──────────┘            
src        └──┘   └──────────┘                       └──┘
typ        └──┘   └──────────┘                  └──┘
doc        └──┘                                       └──┘
txt                                                   └──┘
par                                                   └──┘
st                                                   └───┘
579    sign_eq_sign_of_equiv _ _
id     └───────────────────┘
src    └───────────────────┘
typ    └───────────────────┘
580      (equiv.of_bijective
id        └────────────────┘
src       └────────────────┘
typ       └────────────────┘
581        (show function.bijective (λ x : {x // f x ≠ x},
id               └────────────────┘               
src              └────────────────┘                 
typ              └────────────────┘               
582          (⟨i x.1 x.2, have f (f x) ≠ f x, from mt (λ h, f.injective h) x.2,
id                                      └┘      └────────┘   
src                                             └┘        └────────┘     
typ                                     └┘      └────────┘   
583            by rw [← h _ x.2 this]; exact mt (hi _ _ this x.2) x.2⟩ : {y // g y ≠ y})),
id                            └──┘         └┘  └┘     └──┘                   
src               └────┘ └─┘ └─┘      └────┘└┘   └───┘     └──┘ └┘             
typ               └────┘└─┘└─┘└──┘  └────┘└┘ └┘└───┘└──┘ └──┘└┘           
doc               └────┘ └─┘ └─┘      └────┘     └───┘     └──┘ └┘
txt               └────┘ └─┘ └─┘      └────┘     └───┘     └──┘ └┘
par               └────┘ └─┘ └─┘      └────┘     └───┘     └──┘ └┘
pid                 └──┘ └─┘ └─┘                └───┘     └──┘ └┘
st               └─────────────────┘└──────────────────────────────┘
584          from ⟨λ ⟨x, hx⟩ ⟨y, hy⟩ h, subtype.eq (hi _ _ _ _ (subtype.mk.inj h)),
id                                   └────────┘  └┘          └────────────┘ 
src                                     └────────┘              └────────────┘
typ                                  └────────┘  └┘          └────────────┘ 
585            λ ⟨y, hy⟩, let ⟨x, hfx, hx⟩ := hg y hy in ⟨⟨x, hfx⟩, subtype.eq hx⟩⟩))
id                 └┘   └─┘    └─┘  └┘     └┘                    └────────┘
src                                                                 └────────┘
typ                └┘   └─┘    └─┘  └┘     └┘                    └────────┘
586        (λ ⟨x, _⟩, subtype.eq (h x _ _))
id                  └────────┘  
src                   └────────┘
typ                 └────────┘  
587  ... = sign g : sign_subtype_perm _ _ (λ _, id)
id         └──┘    └───────────────┘          └┘
src        └──┘     └───────────────┘           └┘
typ        └──┘    └───────────────┘          └┘
doc        └──┘
588  
589  def is_cycle (f : perm β) := ∃ x, f x ≠ x ∧ ∀ y, f y ≠ y → ∃ i : ℤ, (f ^ i) x = y
id                     └──┘                                    
src                    └──┘                                               
typ                    └──┘                                    
doc                    └──┘
590  
591  lemma is_cycle_swap {x y : α} (hxy : x ≠ y) : is_cycle (swap x y) :=
id                                             └──────┘  └──┘  
src                                               └──────┘  └──┘
typ                                            └──────┘  └──┘  
doc                                                          └──┘
592  ⟨y, by rwa swap_apply_right,
id             └──────────────┘
src         └──┘└──────────────┘
typ        └──┘└──────────────┘
doc         └──┘
txt         └──┘
par         └──┘
pid            
st         └───────────────────┘
593    λ a (ha : ite (a = x) y (ite (a = y) x a) ≠ a),
id              └─┘        └─┘          
src              └─┘           └─┘             
typ             └─┘        └─┘          
594      if hya : y = a then ⟨0, hya⟩
id       └┘                   └─┘
src      └┘         
typ      └┘                   └─┘
595      else ⟨1, by rw [gpow_one, swap_apply_def]; split_ifs at *; cc⟩⟩
id                      └──────┘  └────────────┘
src                  └──┘└──────┘└┘└────────────┘  └────────────┘  └┘
typ                 └──┘└──────┘└┘└────────────┘  └────────────┘  └┘
doc                  └──┘        └┘                └────────────┘  └┘
txt                  └──┘        └┘                └────────────┘  └┘
par                  └──┘        └┘                └────────────┘  └┘
pid                    └┘        └┘                         └───┘
st                  └───────────┘└──────────────┘└──────────────────┘
596  
597  lemma is_cycle_inv {f : perm β} (hf : is_cycle f) : is_cycle (f⁻¹) :=
id                           └──┘         └──────┘     └──────┘  └┘
src                          └──┘          └──────┘      └──────┘   └┘
typ                          └──┘         └──────┘     └──────┘  └┘
doc                          └──┘
598  let ⟨x, hx⟩ := hf in
id   └─┘    └┘     └┘
typ  └─┘    └┘     └┘
599  ⟨x, by simp [eq_inv_iff_eq, inv_eq_iff_eq, *] at *; cc,
id                └───────────┘  └───────────┘
src         └────┘└───────────┘└┘└───────────┘└───────┘  └┘
typ         └────┘└───────────┘└┘└───────────┘└───────┘  └┘
doc         └────┘             └┘             └───────┘  └┘
txt         └────┘             └┘             └───────┘  └┘
par         └────┘             └┘             └───────┘  └┘
pid                          └┘             └──┘└──┘
st         └──────────────────────────────────────────────┘
600    λ y hy, let ⟨i, hi⟩ := hx.2 y (by simp [eq_inv_iff_eq, inv_eq_iff_eq, *] at *; cc) in
id        └┘  └─┘                          └───────────┘  └───────────┘
src                                     └────┘└───────────┘└┘└───────────┘└───────┘  └┘
typ       └┘  └─┘                    └────┘└───────────┘└┘└───────────┘└───────┘  └┘
doc                                      └────┘             └┘             └───────┘  └┘
txt                                      └────┘             └┘             └───────┘  └┘
par                                      └────┘             └┘             └───────┘  └┘
pid                                                       └┘             └──┘└──┘
st                                      └──────────────────────────────────────────────┘
601      ⟨-i, by rwa [gpow_neg, inv_gpow, inv_inv]⟩⟩
id                   └──────┘  └──────┘  └─────┘
src             └───┘└──────┘└┘└──────┘└┘└─────┘
typ             └───┘└──────┘└┘└──────┘└┘└─────┘
doc              └───┘        └┘        └┘       
txt              └───┘        └┘        └┘       
par              └───┘        └┘        └┘       
pid                 └┘        └┘        └┘       
st              └────────────┘└────────┘└───────┘
602  
603  lemma exists_gpow_eq_of_is_cycle {f : perm β} (hf : is_cycle f) {x y : β}
id                                         └──┘         └──────┘          
src                                        └──┘          └──────┘
typ                                        └──┘         └──────┘          
doc                                        └──┘
604    (hx : f x ≠ x) (hy : f y ≠ y) : ∃ i : ℤ, (f ^ i) x = y :=
id                                          
src                                                 
typ                                         
605  let ⟨g, hg⟩ := hf in
id   └─┘     └┘     └┘
typ  └─┘     └┘     └┘
606  let ⟨a, ha⟩ := hg.2 x hx in
id   └─┘                └┘
src                   
typ  └─┘                └┘
607  let ⟨b, hb⟩ := hg.2 y hy in
id   └─┘                └┘
src                   
typ  └─┘                └┘
608  ⟨b - a, by rw [← ha, ← mul_apply, ← gpow_add, sub_add_cancel, hb]⟩
id                   └┘    └───────┘    └──────┘  └────────────┘  └┘
src            └────┘  └──┘└───────┘└──┘└──────┘└┘└────────────┘└┘  
typ            └────┘└┘└──┘└───────┘└──┘└──────┘└┘└────────────┘└┘└┘
doc             └────┘  └──┘         └──┘        └┘              └┘  
txt             └────┘  └──┘         └──┘        └┘              └┘  
par             └────┘  └──┘         └──┘        └┘              └┘  
pid               └──┘  └──┘         └──┘        └┘              └┘  
st             └───────┘└───────────┘└──────────┘└──────────────┘└──┘
609  
610  lemma is_cycle_swap_mul_aux₁ : ∀ (n : ℕ) {b x : α} {f : perm α}
id                                                        └──┘ 
src                                                         └──┘
typ                                                       └──┘ 
doc                                                          └──┘
611    (hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
id            └──┘                            
src           └──┘                                     
typ           └──┘                            
doc           └──┘
612    ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
id             └──┘                 
src            └──┘                       
typ            └──┘                 
doc               └──┘
613  | 0         := λ b x f hb h, ⟨0, h⟩
id                       └┘       
typ                      └┘       
614  | (n+1 : ℕ) := λ b x f hb h,
id                    └┘ 
src          
typ                   └┘ 
615    if hfbx : f x = b then ⟨0, hfbx⟩
id     └┘                     └──┘
src    └┘            
typ    └┘                     └──┘
616    else
617      have f b ≠ b ∧ b ≠ x, from ne_and_ne_of_swap_mul_apply_ne_self hb,
id       └──┘               └─────────────────────────────────┘ └┘
src                              └─────────────────────────────────┘
typ      └──┘               └─────────────────────────────────┘ └┘
618      have hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b,
id                   └──┘          └┘    └┘ 
src                  └──┘               └┘      └┘
typ                  └──┘          └┘    └┘ 
doc                  └──┘
619        by rw [mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx),
id                └───────┘  └────────────┘  └────────────────────┘ └──┘    └─────┘ └──┘
src           └──┘└───────┘└┘└────────────┘└┘└────────────────────┘    └─┘ └─────┘    └──
typ           └──┘└───────┘└┘└────────────┘└┘└────────────────────┘└──┘└─┘ └─────┘└──┘└──
doc           └──┘         └┘              └┘                          └─┘            └──
txt           └──┘         └┘              └┘                          └─┘            └──
par           └──┘         └┘              └┘                          └─┘            └──
pid             └┘         └┘              └┘                          └─┘            └──
st           └────────────┘└──────────────┘└────────────────────────────────────────────┘└─
620            ne.def, ← injective.eq_iff f.injective, apply_inv_self];
id             └────┘    └──────────────┘ └─────────┘  └────────────┘
src  ─────────┘└────┘└──┘└──────────────┘└─────────┘└┘└────────────┘
typ  ─────────┘└────┘└──┘└──────────────┘└─────────┘└┘└────────────┘
doc  ─────────┘      └──┘                           └┘              
txt  ─────────┘      └──┘                           └┘              
par  ─────────┘      └──┘                           └┘              
pid  ─────────┘      └──┘                           └┘              
st   ───────────────┘└──────────────────────────────┘└──────────────┘└─
621          exact this.1,
id                 └──┘
src          └────┘    └┘
typ          └────┘└──┘└┘
doc          └────┘    └┘
txt          └────┘    └┘
par          └────┘    └┘
pid                   └┘
st   ───────────────────┘
622      let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n hb'
id       └─┘           └────────────────────┘   └─┘
typ      └─┘           └────────────────────┘   └─┘
623        (f.injective $
id          └────────┘
src          └────────┘
typ         └────────┘
624          by rw [apply_inv_self];
id                  └────────────┘
src             └──┘└────────────┘
typ             └──┘└────────────┘
doc             └──┘              
txt             └──┘              
par             └──┘              
pid               └┘              
st             └─────────────────┘└─
625          rwa [pow_succ, mul_apply] at h) in
id                └──────┘  └───────┘
src          └───┘└──────┘└┘└───────┘└────┘
typ          └───┘└──────┘└┘└───────┘└────┘
doc          └───┘        └┘         └────┘
txt          └───┘        └┘         └────┘
par          └───┘        └┘         └────┘
pid             └┘        └┘         └───┘
st   ────────────┘└──────┘└─────────┘└───┘
626      ⟨i + 1, by rw [add_comm, gpow_add, mul_apply, hi, gpow_one, mul_apply, apply_inv_self,
id                     └──────┘  └──────┘  └───────┘  └┘  └──────┘  └───────┘  └────────────┘
src                └──┘└──────┘└┘└──────┘└┘└───────┘└┘  └┘└──────┘└┘└───────┘└┘└────────────┘└─
typ                └──┘└──────┘└┘└──────┘└┘└───────┘└┘└┘└┘└──────┘└┘└───────┘└┘└────────────┘└─
doc                 └──┘        └┘        └┘         └┘  └┘        └┘         └┘              └─
txt                 └──┘        └┘        └┘         └┘  └┘        └┘         └┘              └─
par                 └──┘        └┘        └┘         └┘  └┘        └┘         └┘              └─
pid                   └┘        └┘        └┘         └┘  └┘        └┘         └┘              └─
st                 └───────────┘└────────┘└─────────┘└──┘└────────┘└─────────┘└──────────────┘└─
627          swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (ne.symm hfbx)]⟩
id           └────────────────────┘  └─────────────────────────────────┘ └┘     └─────┘ └──┘
src  ───────┘└────────────────────┘ └─────────────────────────────────┘  └──┘ └─────┘    └┘
typ  ───────┘└────────────────────┘ └─────────────────────────────────┘└┘└──┘ └─────┘└──┘└┘
doc  ───────┘                                                            └──┘            └┘
txt  ───────┘                                                            └──┘            └┘
par  ───────┘                                                            └──┘            └┘
pid  ───────┘                                                            └──┘            └┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘
628  
629  lemma is_cycle_swap_mul_aux₂ : ∀ (n : ℤ) {b x : α} {f : perm α}
id                                                        └──┘ 
src                                                         └──┘
typ                                                       └──┘ 
doc                                                          └──┘
630    (hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
id            └──┘                            
src           └──┘                                     
typ           └──┘                            
doc           └──┘
631    ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
id             └──┘                 
src            └──┘                       
typ            └──┘                 
doc               └──┘
632  | (n : ℕ) := λ b x f, is_cycle_swap_mul_aux₁ n
id                    └────────────────────┘
src                       └────────────────────┘
typ                   └────────────────────┘
633  | -[1+ n] := λ b x f hb h,
id     └──┘          └┘ 
src    └──┘  
typ    └──┘          └┘ 
634    if hfbx : f⁻¹ x = b then ⟨-1, by rwa [gpow_neg, gpow_one, mul_inv_rev, mul_apply, swap_inv, swap_apply_right]⟩
id     └┘        └┘                     └──────┘  └──────┘  └─────────┘  └───────┘  └──────┘  └──────────────┘
src    └┘         └┘                  └───┘└──────┘└┘└──────┘└┘└─────────┘└┘└───────┘└┘└──────┘└┘└──────────────┘
typ    └┘        └┘                └───┘└──────┘└┘└──────┘└┘└─────────┘└┘└───────┘└┘└──────┘└┘└──────────────┘
doc                                     └───┘        └┘        └┘           └┘         └┘        └┘                
txt                                     └───┘        └┘        └┘           └┘         └┘        └┘                
par                                     └───┘        └┘        └┘           └┘         └┘        └┘                
pid                                        └┘        └┘        └┘           └┘         └┘        └┘                
st                                     └────────────┘└────────┘└───────────┘└─────────┘└────────┘└────────────────┘
635    else if hfbx' : f x = b then ⟨0, hfbx'⟩
id          └┘                      └───┘
src         └┘             
typ         └┘                      └───┘
636    else
637    have f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb,
id     └──┘            └─────────────────────────────────┘ └┘
src                         └─────────────────────────────────┘
typ    └──┘            └─────────────────────────────────┘ └┘
638    have hb : (swap x (f⁻¹ x) * f⁻¹) (f⁻¹ b) ≠ f⁻¹ b,
id                └──┘   └┘    └┘   └┘    └┘ 
src               └──┘     └┘      └┘    └┘      └┘
typ               └──┘   └┘    └┘   └┘    └┘ 
doc               └──┘
639      by rw [mul_apply, swap_apply_def];
id              └───────┘  └────────────┘
src         └──┘└───────┘└┘└────────────┘
typ         └──┘└───────┘└┘└────────────┘
doc         └──┘         └┘              
txt         └──┘         └┘              
par         └──┘         └┘              
pid           └┘         └┘              
st         └────────────┘└──────────────┘└─
640        split_ifs;
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
st   ─────────────────
641        simp [inv_eq_iff_eq, eq_inv_iff_eq] at *; cc,
id               └───────────┘  └───────────┘
src        └────┘└───────────┘└┘└───────────┘└────┘  └┘
typ        └────┘└───────────┘└┘└───────────┘└────┘  └┘
doc        └────┘             └┘             └────┘  └┘
txt        └────┘             └┘             └────┘  └┘
par        └────┘             └┘             └────┘  └┘
pid                         └┘             └──┘
st   ─────────────────────────────────────────────────┘
642    let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n hb
id     └─┘           └────────────────────┘   └┘
src                   └────────────────────┘
typ    └─┘           └────────────────────┘   └┘
643      (show (f⁻¹ ^ n) (f⁻¹ x) = f⁻¹ b, by
id              └┘      └┘    └┘ 
src              └┘       └┘      └┘
typ             └┘      └┘    └┘ 
st                                          
644        rw [← gpow_coe_nat, ← h, ← mul_apply, ← mul_apply, ← mul_apply, gpow_neg_succ, ← inv_pow, pow_succ', mul_assoc,
id               └──────────┘        └───────┘    └───────┘    └───────┘  └───────────┘    └─────┘  └───────┘  └───────┘
src        └────┘└──────────┘└──┘ └──┘└───────┘└──┘└───────┘└──┘└───────┘└┘└───────────┘└──┘└─────┘└┘└───────┘└┘└───────┘└─
typ        └────┘└──────────┘└──┘└──┘└───────┘└──┘└───────┘└──┘└───────┘└┘└───────────┘└──┘└─────┘└┘└───────┘└┘└───────┘└─
doc        └────┘            └──┘ └──┘         └──┘         └──┘         └┘             └──┘       └┘         └┘         └─
txt        └────┘            └──┘ └──┘         └──┘         └──┘         └┘             └──┘       └┘         └┘         └─
par        └────┘            └──┘ └──┘         └──┘         └──┘         └┘             └──┘       └┘         └┘         └─
pid          └──┘            └──┘ └──┘         └──┘         └──┘         └┘             └──┘       └┘         └┘         └─
st   ───────────────────────┘└───┘└───────────┘└───────────┘└───────────┘└─────────────┘└─────────┘└─────────┘└─────────┘└─
645          mul_assoc, inv_mul_self, mul_one, gpow_coe_nat, ← pow_succ', ← pow_succ]) in
id           └───────┘  └──────────┘  └─────┘  └──────────┘    └───────┘    └──────┘
src  ───────┘└───────┘└┘└──────────┘└┘└─────┘└┘└──────────┘└──┘└───────┘└──┘└──────┘
typ  ───────┘└───────┘└┘└──────────┘└┘└─────┘└┘└──────────┘└──┘└───────┘└──┘└──────┘
doc  ───────┘         └┘            └┘       └┘            └──┘         └──┘        
txt  ───────┘         └┘            └┘       └┘            └──┘         └──┘        
par  ───────┘         └┘            └┘       └┘            └──┘         └──┘        
pid  ───────┘         └┘            └┘       └┘            └──┘         └──┘        
st   ────────────────┘└────────────┘└───────┘└────────────┘└───────────┘└──────────┘
646    have h : (swap x (f⁻¹ x) * f⁻¹) (f x) = f⁻¹ x, by rw [mul_apply, inv_apply_self, swap_apply_left],
id               └──┘   └┘    └┘       └┘          └───────┘  └────────────┘  └─────────────┘
src              └──┘     └┘      └┘          └┘       └──┘└───────┘└┘└────────────┘└┘└─────────────┘
typ              └──┘   └┘    └┘       └┘      └──┘└───────┘└┘└────────────┘└┘└─────────────┘
doc              └──┘                                    └──┘         └┘              └┘               
txt                                                      └──┘         └┘              └┘               
par                                                      └──┘         └┘              └┘               
pid                                                        └┘         └┘              └┘               
st                                                      └────────────┘└──────────────┘└───────────────┘
647    ⟨-i, by rw [← add_sub_cancel i 1, neg_sub, sub_eq_add_neg, gpow_add, gpow_one, gpow_neg, ← inv_gpow,
id                  └────────────┘     └─────┘  └────────────┘  └──────┘  └──────┘  └──────┘    └──────┘
src           └────┘└────────────┘ └──┘└─────┘└┘└────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└──┘└──────┘└─
typ           └────┘└────────────┘└──┘└─────┘└┘└────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└──┘└──────┘└─
doc            └────┘               └──┘       └┘              └┘        └┘        └┘        └──┘        └─
txt            └────┘               └──┘       └┘              └┘        └┘        └┘        └──┘        └─
par            └────┘               └──┘       └┘              └┘        └┘        └┘        └──┘        └─
pid              └──┘               └──┘       └┘              └┘        └┘        └┘        └──┘        └─
st            └──────────────────────┘└────────┘└──────────────┘└────────┘└────────┘└────────┘└──────────┘└─
648        mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x, gpow_add, gpow_one,
id         └─────────┘  └──────┘  └──────────────────┘  └────────────┘  └───────┘     └──────┘  └──────┘
src  ─────┘└─────────┘└┘└──────┘└┘└──────────────────┘└┘└────────────┘└┘└───────┘└─┘ └┘└──────┘└┘└──────┘
typ  ─────┘└─────────┘└┘└──────┘└┘└──────────────────┘└┘└────────────┘└┘└───────┘└─┘└┘└──────┘└┘└──────┘
doc  ─────┘           └┘        └┘                    └┘              └┘         └─┘ └┘        └┘
txt  ─────┘           └┘        └┘                    └┘              └┘         └─┘ └┘        └┘
par  ─────┘           └┘        └┘                    └┘              └┘         └─┘ └┘        └┘
pid  ─────┘           └┘        └┘                    └┘              └┘         └─┘ └┘        └┘
st   ────────────────┘└────────┘└────────────────────┘└──────────────┘└─────────────┘└────────┘└────────┘
649        mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx')]⟩
id                                              
src                                            
typ                                            
doc                                            
txt                                            
par                                            
pid                                            
st                                             └┘                                                                       
650  
651  lemma eq_swap_of_is_cycle_of_apply_apply_eq_self {f : perm α} (hf : is_cycle f) {x : α}
id                                                                                      
typ                                                                                     
652    (hfx : f x ≠ x) (hffx : f (f x) = x) : f = swap x (f x) :=
id                                                
typ                                               
653  equiv.ext _ _ $ λ y,
id                     
typ                    
654  let ⟨z, hz⟩ := hf in
id                  └┘
typ                 └┘
655  let ⟨i, hi⟩ := hz.2 x hfx in
id                       
typ                      
656  if hyx : y = x then by simp [hyx]
id                              └─┘
typ                             └─┘
657  else if hfyx : y = f x then by simp [hfyx, hffx]
id                      
typ                     
658  else begin
659    rw [swap_apply_of_ne_of_ne hyx hfyx],
id                                └─┘
typ                               └─┘
660    refine by_contradiction (λ hy, _),
661    cases hz.2 y hy with j hj,
id                
typ               
662    rw [← sub_add_cancel j i, gpow_add, mul_apply, hi] at hj,
id                           
typ                          
663    cases gpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji hji,
id                                                         
typ                                                        
664    { rw [← hj, hji] at hyx, cc },
st                                 └┘
665    { rw [← hj, hji] at hfyx, cc }
st                                  └┘
666  end
667  
668  lemma is_cycle_swap_mul {f : perm α} (hf : is_cycle f) {x : α}
id                                                             
typ                                                            
669    (hx : f x ≠ x) (hffx : f (f x) ≠ x) : is_cycle (swap x (f x) * f) :=
id                                                          
typ                                                         
670  ⟨f x, by simp only [swap_apply_def, mul_apply];
id     
typ    
671          split_ifs; simp [injective.eq_iff f.injective] at *; cc,
id                                                                └┘
src                                                               └┘
typ                                                               └┘
doc                                                               └┘
672    λ y hy,
id       
typ      
673    let ⟨i, hi⟩ := exists_gpow_eq_of_is_cycle hf hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1 in
id                                              └┘
typ                                             └┘
674    have hi : (f ^ (i - 1)) (f x) = y, from
id                                  
typ                                 
675      calc (f ^ (i - 1)) (f x) = (f ^ (i - 1) * f ^ (1 : ℤ)) x : by rw [gpow_one, mul_apply]
id                                                        
src                                                         
typ                                                       
st                                                                                            
676      ... =  y : by rwa [← gpow_add, sub_add_cancel],
id              
typ             
677    is_cycle_swap_mul_aux₂ (i - 1) hy hi⟩
678  
679  @[simp] lemma support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support = {x, y} :=
id                               └──┘                                                  
src                              └──┘  
typ                              └──┘                                                  
doc    └──┘                      └──┘  
680  finset.ext.2 $ λ a, by simp [swap_apply_def]; split_ifs; cc
id                                                           └┘
src                                                           └┘
typ                                                          └┘
doc                                                           └┘
681  
682  lemma card_support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support.card = 2 :=
id                            └──┘                                   
src                           └──┘  
typ                           └──┘                                   
doc                           └──┘  
683  show (swap x y).support.card = finset.card ⟨x::y::0, by simp [hxy]⟩,
id                                                             └─┘
typ                                                            └─┘
684  from congr_arg card $ by rw [support_swap hxy]; simp [*, finset.ext]; cc
id                                             └─┘                         └┘
src                                                                        └┘
typ                                            └─┘                         └┘
doc                                                                        └┘
685  
686  lemma sign_cycle [fintype α] : ∀ {f : perm α} (hf : is_cycle f),
id                     └──┘                                    
src                    └──┘  
typ                    └──┘                                    
doc                    └──┘  
687    sign f = -(-1 ^ f.support.card)
id                    
typ                   
688  | f := λ hf,
id            └┘
typ           └┘
689  let ⟨x, hx⟩ := hf in
id                  └┘
typ                 └┘
690  calc sign f = sign (swap x (f x) * (swap x (f x) * f)) :
691    by rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]
st                                                                
692  ... = -(-1 ^ f.support.card) :
693    if h1 : f (f x) = x
694    then
695      have h : swap x (f x) * f = 1,
696        by conv in (f) {rw eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx.1 h1 };
id                                                                       └┘
typ                                                                      └┘
697          simp [mul_def, one_def],
698      by rw [sign_mul, sign_swap hx.1.symm, h, sign_one, eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx.1 h1,
id                                                                                                     └┘
typ                                                                                                    └┘
699          card_support_swap hx.1.symm]; refl
id                                         └──┘
src                                        └──┘
typ                                        └──┘
doc                                        └──┘
700    else
701      have h : card (support (swap x (f x) * f)) + 1 = card (support f),
702        by rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq h1,
703          card_insert_of_not_mem (not_mem_erase _ _)],
st                                                     
704      have wf : card (support (swap x (f x) * f)) < card (support f),
705        from card_support_swap_mul hx.1,
706      by rw [sign_mul, sign_swap hx.1.symm, sign_cycle (is_cycle_swap_mul hf hx.1 h1), ← h];
id                                                                           └┘
typ                                                                          └┘
707        simp [pow_add]
708  using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, f.support.card)⟩]}
id                                     
typ                                    
709  
710  end sign
711  
712  end equiv.perm
713  
714  lemma finset.prod_univ_perm [fintype α] [comm_monoid β] {f : α → β} (σ : perm α) :
id                                └┘  └─┘     └┘ └┘ └┘                         
src                               └┘  └─┘      └┘ └┘ └┘ 
typ                               └┘  └─┘     └┘ └┘ └┘                         
doc                               └┘  └─┘
715    (univ : finset α).prod f = univ.prod (λ z, f (σ z)) :=
id             └┘  └┘                              
src            └┘  └┘
typ            └┘  └┘                              
doc            └┘  └┘
716  eq.symm $ prod_bij (λ z _, σ z) (λ _ _, mem_univ _) (λ _ _, rfl)
id                                                       
typ                                                      
717    (λ _ _ _ _ H, σ.injective H) (λ b _, ⟨σ⁻¹ b, mem_univ _, by simp⟩)
id                                           
typ                                          
718  
719  lemma finset.sum_univ_perm [fintype α] [add_comm_monoid β] {f : α → β} (σ : perm α) :
id                               └──┘      └┘ └┘ └┘ └┘ └┘                        
src                              └──┘       └┘ └┘ └┘ └┘ └┘
typ                              └──┘      └┘ └┘ └┘ └┘ └┘                        
doc                              └──┘  
720    (univ : finset α).sum f = univ.sum (λ z, f (σ z)) :=
id             └┘  └┘                            
src            └┘  └┘
typ            └┘  └┘                            
doc            └┘  └┘
721  @finset.prod_univ_perm _ (multiplicative β) _ _ f σ
id                                                   
typ                                                  
722  
723  attribute [to_additive] finset.prod_univ_perm
doc              └───────┘